- Author
- Jonathan Aldrich
- Published
- Undated
- Kind
- University lecture notes, with one worked proof
- Original
- www.cs.cmu.edu/~aldrich/courses/654-sp09/notes/3-hoare-notes.pdf
- Subject
- Formal methods and proof
What it is
Jonathan Aldrich wrote the notes for course 17-654/17-754. They introduce partial and total correctness, weakest preconditions and loop invariants. The aim is to let students prove small programs correct by hand.
What it says
- The notes treat a specification as a contract between a function and its clients. The precondition binds the client, and the postcondition binds the function.
- Total correctness is partial correctness plus termination.
- If a client breaks the precondition, the function may behave in any way. A function meant to survive bad input should include it in the precondition.
- A triple can be correct yet weak. For x := x*2 from x = 5, the strongest postcondition is x = 10.
- Proving a loop correct needs an invariant. Proving that it terminates also needs an integer variant function.
- A worked power program gets its invariant by replacing m with i in the postcondition. The notes then add bounds until the proof works.
What evidence it gives
The notes give definitions and one worked example. The example is a loop that computes a power. The notes list each proof obligation and prove it with short justified steps. They offer no experiments.
Interests and limits
The notes are short and written for students. They omit the strongest postcondition function and call it beyond their scope. The proof covers one small program in a toy language. The notes do not say how well the method scales.