Proof of Program Correctness

EXAMPLE:

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) < b(j) then
    c(k):=a(i);
    i := i+1;
  else
    c(k):=b(j);
    j := j+1;
  end if;
  k:=k+1;
end loop;