On the proof of correctness of a calendar program
Leslie Lamport · Communications of the ACM · 1979
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.