The evolution of programs: Program abstraction and instantiation
Nachum Dershowitz · International Conference on Software Engineering · 1981
Our goal is to develop techniques for abstracting a given set of concrete programs into a program schema and for instantiating a schema to satisfy concrete specifications. For example, from two programs using the binary-search method, one to compute quotients and another to compute cube-roots, an abstract schema is derived that embodies the method and that can be instantiated to solve similar new problems.We suggest the formulation of analogies as a basic tool in program abstraction. An analogy is first sought between the specifications of the given programs; this yields an abstract specification that may be instantiated to any of the given concrete specifications. The analogy is then used as a basis for transforming the existing programs into an abstract schema that represents the embedded technique. The invariant assertions and correctness proofs of the given programs are used to complete the analogy.