The scope of program verification techniques can be extended beyond their original goals which was verifying correctness of individual programs. Assuming correctness of an implementation, axioms for a required data structure can be inferred. If these axioms are not contradictory, the data structure can be implemented in a second step, applying the same method again.
Mechanical program verifiers play an essential role in that task. They can be designed to handle abstract program schemata and thereby aid theoretical understanding and discussion of the mathematical foundations and interrelations.