Nachum Dershowitz
ABSTRACT
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.
- 1.R. Brown {Oct. 1976}, Reasoning by analogy, Working paper 132, Artificial Intelligence Laboratory, MIT, Cambridge, MA.]]Google Scholar
- 2.T.W. Chen and N.V. Findler {Dec. 1976}, Toward analogical reasoning in problem solving by computers, Technical report 115, Dept. of Computer Science, State Univ. of New York, Buffalo, NY.]]Google Scholar
- 3.J. Darlington and R.M. Burstall {Mar. 1976}, A system which automatically improves programs, Acta Informatica, vol. 6, no. 1, pp. 41-60.]]Google ScholarDigital Library
- 4.N. Dershowitz {Nov. 1978}, The evolution of programs, Ph.D. thesis, Dept. of Applied Mathematics, Weizmann Inst. of Science, Rehovot, Israel; available as Report R-80-1011, Dept. of Computer Science, Univ. of Illinois, Urbana, IL.]]Google Scholar
- 5.N. Dershowitz and Z. Manna {July 1975}, On automating structured programming, Proc. Colloq. IRIA on Proving and Improving Programs, Arc-et-Senans, France.]]Google Scholar
- 6.N. Dershowitz and Z. Manna {Nov. 1977}, The evolution of programs: Automatic program modification, IEEE Software Engineering, vol. SE-3, no. 6, pp. 377-385.]]Google Scholar
- 7.E.W. Dijkstra {1972}, Notes on structured programming, in O.J. Dahl, E.W. Dijkstra, and C.A.R. Hoare, Structured Programming, Academic Press, London.]] Google ScholarDigital Library
- 8.A.G. Duncan and L. Yelowitz {July 1979}, Studies in abstract/concrete mappings in proving algorithm correctness, Proc. Sixth EATCS Colloq. on Automata, Languages and Programming, Graz, Austria, pp. 218-229.]] Google ScholarDigital Library
- 9.S.L. Gerhart {Apr. 1975}, Knowledge about programs: A model and case study, Proc. Intl. Conf. on Reliable Software, Los Angeles, CA, pp. 88-95.]] Google ScholarDigital Library
- 10.S.L. Gerhart and L. Yelowitz {Dec. 1976}, Control structure abstractions of the backtracking programming technique, IEEE Software Engineering, vol. SE-2, no. 4, pp. 285-292.]]Google Scholar
- 11.G. Huet and B. Lang {Dec. 1978}, Proving and applying program transformations expressed with second-order patterns, Acta Informatica, vol. 11, no. 1, pp. 31-55.]]Google ScholarDigital Library
- 12.R.E. Kling {Aug. 1971}, Reasoning by analogy with applications to heuristic problem solving: A case study, Ph.D. thesis, Stanford Univ., Stanford, CA.]] Google ScholarDigital Library
- 13.Z. Manna and R.J. Waldinger {Summer 1975}, Reasoning and knowledge in program synthesis, Artificial Intelligence, vol. 6, no. 2, pp. 175-208.]]Google ScholarCross Ref
- 14.J. Misra {Sept. 1978}, An approach to formal definitions and proofs of programming principles, IEEE Software Engineering, vol. SE-4, no. 5, pp. 410-413.]]Google Scholar
- 15.D.A. Plaisted {July 1980}, Abstraction mappings in mechanical theorem proving, Proc. Fifth Conf. on Automated Deduction, Les Arcs, France, pp. 264-280.]] Google ScholarDigital Library
- 16.G.J. Sussman {1975}, A computer model of skill acquisition, American Elsevier, New York.]] Google ScholarDigital Library
- 17.J.W. Ulrich and R. Moll {Aug. 1977}, Program synthesis by analogy, Proc. ACM Symp. on Artificial Intelligence and Programming Languages, Rochester, NY, pp. 22-28.]] Google ScholarDigital Library
- 18.L. Yelowitz and A.G. Duncan {Aug. 1977}, Abstractions, instantiations and proofs of marking algorithms, Proc. ACM Symp. on Artificial Intelligence and Programming Languages, Rochester, NY, pp. 13-21.]] Google ScholarDigital Library
Index Terms
- The evolution of programs: Program abstraction and instantiation
Recommendations
Correctness of logic programs using proof schemes
The correctness of logic programs which are constructed by a schema-based method is presented in this paper. This schema-based method constructs typed, moded logic programs by stepwise top-down design using five program schemata, data types and modes. ...
Proving termination of context-sensitive rewriting by transformation
Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite ...
Knowledge about programs: A model and case study
International Conference on Reliable SoftwareDijkstra suggests in his “Notes on Structured Programming” that program schema and theorems about their correctness may describe the way that programmers understand programming. This paper follows up his suggestion by describing a general model for ...
Comments