Design and Analysis of Algorithms

Design by Proof Rules 165

As an example of a situation requiring the weak form of the fi rst condition in the loop termination

lemma, that is, I ⇒ (B ⇒ 0 < v), consider a loop for processing every element of a two dimensional array

B(j, k) where the index j varies between 1 to N

j

inclusive and index k between 1 to N

k

inclusive. If the

loop invariant I contains the terms 1 ≤ N

j

∧ 1 ≤ N

k

∧ j ≤ N

j

∧ k ≤ N

k

and if the while condition B is

(j < N

j

∨ k < N

k

), then one suitable loop variant function v is N

j

* (N

k

– k) + (N

j

– j). B independently does

not imply that v is positive; I is also essential to show that v is positive.

7.4 A SIMPLE DESIGN PROCEDURE ...