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