Design and Analysis of Algorithms

132 Design and Analysis of Algorithms

loop. Also, P ∧ B holds every time at C. When the loop terminates, P ∧ ¬B holds at the point D. So we get

our proof rule:

{P ∧ B} S {P} / {P} while B do S {P ∧ ¬B}

B

P

False

True

A

D

S

C

P

here B may or may not be True

P

Ù Ø B

P

Ù B

Fig. 6.7 Deriving the proof rule for while-do

Note that this proof rule establishes an invariant property P for the loop. P is referred to as the loop

invariant.

6.4.5 Repeat-Until Statement

This construct has the form:

repeat S until B in PASCAL and do {S1}; while(expr); in C.

See Fig. 6.8. The proof rule can be derived by using considerations similar to the case of while-do.

We directly ...