Invariant {P} : Predicate that is true throughout the program

• Invariant {P} : Predicate that is true throughout the program

• Guard Bi, BB:

  • True on entry into the loop
  • May be true or false at the exit point of the loop => re-evaluate guard
  • The guard is always false after the loop terminates
  • Postcondition {R}: The postcondition should imply the Invariant and the negation of the guard i.e. P ? ?BB => R
  • Precondition{Q}: Should imply the Invariant with initialisations.

Previous slide

Next slide

Back to first slide

View graphic version