The loop rule proves safety of a loop [a*]P by a loop invariant J:

  1. initial case: J is true initially
  2. use case: J implies the postcondition P
  3. induction step: J is still true after one round of the loop whenever J was true before
Make sure the loop invariants transports enough knowledge about how the state changed during past iterations of a*.

See also

Learning resources