Prove the following program is correct:

{count = 2}
sum = 0;
sum = sum + count;
count = count -1;
sum = sum + count;
{sum = 1 + 2}