Synopsis

• 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.

Sections Covered