EXAMPLE OF USING CORRECTNESS PROOFS IN PRACTICE

The following incorrect program merges
two sorted arrays of n elements each:

i:=1; j;=1; k:=1;
while k =< 2*n loop
if a(i) c(k):=a(i);
i := i+1;
else
c(k):=b(j);
j := j+1;
end if;
k:=k+1;
end loop;