[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

Is I a Loop Invariant?

• Does {y ? x} satisfy the 5 conditions?

(1) {y <= x} => {y <= x} ?

(2) if {y <= x} and y <> x is then evaluated, is {y <= x} still true?

(3) if {y <= x} and y <> x are both true and then y := y+1 is executed, is {y <= x} true?

(4) does {y <= x} and {y = x} => {y = x}?

• Can you argue convincingly that the program segment terminates?