Example: Gauss

As a further example, we consider a program adding all natural numbers below a fixed number N. A correctly annotated program (annotations are enclosed in braces ) is:

        { N > 0 }
        begin
          i   := 0 ;
          sum := 0 ;
          while i < N do { sum = i*(i+1)/2 and i <= N }
            begin
              i   := i+1;
              sum := sum + i
            end
        end
        { sum = N*(N+1)/2 }

Aside from the pre- and postcondition the program contains as annotation a loop invariant. Whilst the principal conjunct of this invariant seems clear, the second conjunct, i <= N would typically be forgotten in a first proof attempt. The resulting verification condition

        sum=i*(i+1)/2 and i >= N   ==>   sum=N*(N+1)/2

is not a tautology. Strengthening the invariant by and i <= N yields i = N in the premise, and the tautology is automatically proved by the system. In fact, NPPV proves all verification conditions except for one :

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

This means that NPPV cannot decide whether the formula

is a tautology in the data structure. Since we have not specified whether i and N are supposed to be integers (so far they might be assumed real), we see that it is perfectly correct, for NPPV to leave us with the above verification condition. All that is by default assumed for the algebraic operations +, -, *, 0, and 1 is that they satisfy the axioms of a commutative ring with unit.