Thread: Program Correctness Proof

Can someone please help!!
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}

Hello vexiked

Originally Posted by vexiked

Can someone please help!!
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.

Grandad