WHILE STATEMENT: AN EXAMPLE



 Start from Post-condition and replace sum by sum+i to obtain:

 { sum + i = 0.5 i (i+1)}

 Move the term i to the right side to obtain:

 { sum = 0.5 (i-1) i }

 Next, replace i by i + 1 to obtain:

 { sum = 0.5 (i+1-1) (i+1) }

 This is the Pre-condition, which is the same as the Post-condition.