Skip to main content
Logo image

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.

Sections Covered.