[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

Using Loop Criterion 4

• Try guessing invariant using criterion 4:

• {I and (not B)} => Q

• I? and y >= x + 1 => y > 5

• I? and y > x => y > 5

• any x >= 5 satisfies implication

• so . . . let I = {x >= 5}

• Do the 4 Axioms hold?