How to prove the ff program?

[dualshock03]

How to prove the following program if it is correct... using some kind of BNF solving... Please need help!!

problem program:

{n>0}

count = n;
sum > sum + count;
while count <> 0 do
sum = sum + count;
count = count - 1;
end


{sum = 1+2+...+n}
-------------------------------------------------
not sure answer is: count>=1

[toptony]

:)

using "typedef" to replace some statements;

a syntax game!

[exception]

Huh? Where is the BNF? And what property do you want to prove?

[dualshock03]

the whole code .. i mean if the output of this code will be correct or reliable or it will just return an error on result..

if anyone knows about this, please post as you can..

[dualshock03]

what about the "typedef"? which statements to be replace??