EXAMPLE OF USING CORRECTNESS PROOFS IN PRACTICE (continued)

The assertion L
{1=< i =< n and 1 =< j =< n and
1 =< k =< 2*n }
CANNOT be verified to be a loop invariant!!!

In fact, L and { k = i+j-1} does NOT imply

{1=< i+1 =< n and 1 =< j+1 =< n and
1 =< k+1 =< 2*n } !!!

Such partial formal analysis can show the
above program has errors. We can thus
localize and repair such errors.