Program Correctness Proof

• Feb 24th 2009, 01:30 PM
vexiked
Program Correctness Proof
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}
• Feb 24th 2009, 10:12 PM
Program proof
Hello vexiked
Quote:

Originally Posted by vexiked
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}

I'm assuming that you're writing this in pseudocode, rather than any specific language. Then it will work OK, provided the end statement is the usual one that you use to end the while loop. Some writers might prefer to use something like end while or end do here.

The other small point is that I notice that you've written each statement (except this one and the while statement) ending with a semi-colon. Whereas I wouldn't expect one at the end of the while line, I might have expected one after end. Was that deliberate or did you forget one here? Otherwise, it's fine.