NPPV does not restrict the user to a fixed set of data structures. New operations and relations may be freely introduced. This feature opens the door to verifying not just fixed programs, but rather general program transformations.
As an example consider the transformation from recursive into sequential programs. Recursive programs are usually easier to specify than sequential ones, but recursive executions often require extra resources in time and space. Therefore, many methods have been invented to transform recursive programs into sequential ones. As a first example we will here only consider the transformation of tail-recursive programs into sequential ones.
Consider the recursive definition of a function f in terms of already available functions g,r and a relation P. The recursive definition is tail-recursive, if it is of the form
An imperative program to compute the same function f is given below. It has already been annotated with the proper pre- and postconditions and a loop- invariant.
{ x = M }
WHILE not P(x) DO { f(x) = f(M) }
x := r(x);
x := g(x)
{ x = f(M) }
The verification conditions generated by NPPV are :
P(x) => f(x)=g(x)
not P(x) => f(x)=f(r(x)),
which is precisely the requirement of tail-recursivity.