Prove the following program is correct, with Axiomatic semantics:

{ n > 0 } (precondition)

count = n;

sum = 0;

while count != 0 do

sum = sum + count;

count = count - 1;

end

{sum = 1 + 2 + . + n} (postcondition)