On the Proof of Correctness of a Calendar Program A formal specification is given for a simple calendar program, and the derivation and proof of correctness of the program are sketched. The specification is easy to understand, and its correctness is manifest to humans. CACM October,1979 Lamport, L. Program specification, program verification, inductive assertions 5.24 CA791003 DB January 16, 1980 5:02 PM 3170 4 3170 3170 4 3170 3055 5 3170 3104 5 3170 3170 5 3170 3170 5 3170 3170 5 3170