[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

More on Loop Invariants

• The loop invariant I is:
  • A weakened version of the loop postcondition, and
  • Also the loop's precondition

• I must be:
  • Weak enough to be satisfied prior to the beginning of the loop, but
  • when combined with the loop exit condition, it must be strong enough to force the truth of the postcondition