Section C.26 V2: Loop Invariants and Mechanizing Verification
- Introduce loop invariants as assertions that hold before and after loop body.
- Reason about correctness of while loop informally.
- Note that loop invariants have to be provided by the programmer.
- As a simple example prove correct the division algorithm.
- Introduce pc and vc functions to generate verification conditions.
- Show their correctness for while and if.
- Demonstrate verification condition generation for division algorithm.