Abstract invariants

The last example shows quite clearly, that it is futile to hope for a widely applicable method for finding proper invariants. Still there are ways to proceed and a verifier may be helpful in this. Firstly, given a specification and a program we may use as invariant an abstract predicate where are all variables occurring in the program. The verifier will then generate a set of verification conditions and the problem becomes to show that they are not contradictory.

In case where a program C is to compute a function f(x), the specification will typically be . A while-loop calculating f(A) will modify x,z and perhaps some auxiliary variables, but maintain an invariant specifying how at each moment f(A) can be recovered from x,z, and the auxiliary variables. With an abstract function r, then should be attempted as an invariant, where the `` '' stand for the auxiliary variables.

The resulting verification conditions can be seen as a set of axioms for a data structure required to make the algorithm work. If a data structure exists making these axioms true, then the program can be accepted as a correct implementation of the specification. The next step will be to implement the data structure conforming to the axioms.

In the following we apply this method in showing how an arbitrary linearly recursive function may be implemented by a sequential program with the aid of a stack. To be specific, a function f is linear recursive, if it is of the form

An example of a linear recursive function is the previously discussed function sumTo. Moreover, every primitive recursive function is linearly recursive. The following program purports to implement the function f in general, using a stack. We have annotated the loops with invariants stating that in the first loop, f(A) can somehow be recovered from f(x) and s (by some as yet unknown function prod) whereas during execution of the second loop, f(A) is recoverable in the same way from z and s.

        { x = A }
        BEGIN
          s := empty;
          WHILE not P(x) DO { prod(f(x),s) = f(A) }
            BEGIN
              s := push(x,s);
              x := r(x)
            END ;
          z := g(x);
          WHILE s <> Empty DO { prod(z,s) = f(A) }  
            BEGIN
              z := h(z,top(s));
              s := pop(s)
            END
        END
        { z = f(A) }

To simplify matters, let us assume that the axioms for the ``stack''-data type, are known to NPPV (in practice, they can be supplied in a ``theory file''), then we remain with the verification conditions :

        prod(x,empty) = x
        prod(x,push(y,s)) = prod(h(x,y),s)

These equations can be considered as the defining equations for the unknown function prod. From the freeness axioms for the stack-operations empty and push it follows that they unambiguously define a total function. Thus we have shown that a proper invariant for the program exists, which is all we need to know.