Gauss

Recall that the proof of the summation program succeeded automatically except for one verification condition that NPPV could not prove. This was the condition

        i < N => i+1 <= N.

All that NPPV assumes about the operations +,* and the relations <, resp. , is that they form an ordered commutative ring with unit. The unproved verification condition can be thus interpreted as an axiom for the data structure needed to make the program work. In other words, the unproved property tells us that Gauss's summation formula is true provided the ring carries a discrete order.

For good reasons one might argue that we have proven Gauss's theorem rather than simply proving that the program sums all numbers up to N. So what we actually should be specifying in the postcondition is that

Since the -operator is not defined in NPPV, we simply specify in the postcondition :

        { sum = sumTo(N) }

and in the invariant :

        { sum=sumTo(i) and  i <= N }.

In addition to the previous

        i < N ==> i+1 <= N

NPPV now generates the two conditions :

        sumTo(0)= 0
        i < N => sumTo(i+1) = sumTo(i)+i

which we are ready to accept as the definition of the summation operator.