Prove the following program is correct:

{n > 0}

count = n;

sum = 0;

while count <> 0 do

sum = sum + count;

count = count - 1;

end

{sum = 1 + 2 + . . . + n}