According to standard definitions [4], an algorithm is a detailed and explicit instruction for the stepwise solution of a given problem. This means that there must be given a repertoire of elementary (or atomic) steps which are to be combined according to the instructions of the algorithm. In a general sense it is of course allowed to think of atomic steps such as ``add a cup of flour'', ``stir'', and of combinations of instructions such as ``add a cup of flour then stir until smooth'', but we shall not deal with recipes, rather with algorithms computing functions over sets of data.
Here an atomic step consists of calculating a data value according to a given set of operations and storing the result in a memory cell. In describing how to combine such elementary steps a small set of instructions including composition ( ; ), conditional (if-then-else) and loops (while or repeat) is commonly used.
This way a separation of concerns is achieved. A data structure defines the admissible atomic steps and a control structure determines how these steps are to be combined to yield the desired algorithm. This view is stated very succinctly in the well known slogan ``algorithm = data structure + control''.
The border separating data structure and control may slide towards
either side depending on the application. As an example we may assume to have
multiplication `` 
'' of natural numbers available as elementary arithmetical
instruction, yet we may also get by with the operators of Presburger
arithmetic (0,succ,+,<) and construct an algorithm for multiplication.
All programming languages provide mechanisms to augment the data structure by
such defined functions.
The main purpose of this article is a demonstration together with a set of some succinct examples that show how Wirth's ``equation'' may be solved for an unknown data structure too. That is, given the specification of an algorithm and given a control structure, automatically determine axioms for a data structure required to fulfil the specification. A vehicle for finding these examples is a program verifier (NPPV) that we have constructed for educational purposes and used in many courses on program verification. With its help we can not only semi-automatically verify concrete programs, but also investigate ``abstract programs'' and reveal relationships between programs, specifications, invariants and data structure requirements. As a simple example, for instance, we shall show that a program to interchange the value of two variables works correctly precisely if the data structure contains a quasigroup operation, or that the failure of a program to find a counterexample to a conjecture leads to an induction axiom for the data type.
NPPV (New Paltz Program Verifier), has been implemented on an IBM compatible PC and
has been developed for, and successfully used in courses devoted to the mathematics
of program verification and abstract data types. The software is embedded in an
``integrated development environment'' with built-in editor, pull-down menus and pop-up
windows. It is freely available for demonstration and course use.