NPPV's proof-component will either succeed in proving a given verification condition, or simplify it to a (hopefully) simpler but logically equivalent statement. It will not force the user to prove these remaining statements, rather collect them into an ``axioms file''.
This gives rise to a novel perspective on program verification. Given a program
together with an appropriate annotation, a set of data structure axioms will
be generated such that
the algorithm satisfies the specification
the data structure axioms are satisfied.
Thus, given a desired algorithm, a data structure may be tailored so that the
algorithm computes the desired function. We shall give a number of examples.