This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fundamentals of Deductive Program Synthesis
August 1992 (vol. 18 no. 8)
pp. 674-704

An informal tutorial for program synthesis is presented, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, the authors prove the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive, in the sense that, in establishing the existence of the desired output, the proof is forced to indicate a computational method for finding it. That method becomes the basis for a program that can be extracted from the proof. The exposition is based on the deductive-tableau system, a theorem-proving framework particularly suitable for program synthesis. The system includes a nonclausal resolution rule, facilities for reasoning about equality, and a well-founded induction rule.

[1] P. B. Andrews "Theorem proving via general matings,"J. ACM, vol. 28, no. 2, pp. 193-214, 1981.
[2] W. Bibel, "Matings in matrices,"Commun. ACM, vol. 26, pp. 844-852, 1983.
[3] R. M. Burstall and J. Darlington, "A transformation system for developing recursive programs,"J. ACM, vol. 24, no. 1, pp. 44-67, Jan. 1977.
[4] W. W. Bledsoe and L. Hines, "Variable elimination and chaining in a resolution-based prover for inequalities," inProc. 5th Conf. on Auto. Deduction, 1980, pp. 281-292.
[5] R. S. Boyer and J. S. Moore,A Computational Logic. New York: Academic Press, 1979.
[6] R. Burback,et al., "Using the deductive tableau system," inMacintosh Educational Software Collection, Chariot Software Group, 1990.
[7] R. L. Constableet al., Implementing Mathematics with the Nuprl Proof Development System. Englewood Cliffs, NJ: Prentice-Hall, 1986.
[8] T. Coquand and G. Huet, "The calculus of constructions,"Inform. Contr., vol. 76, nos. 2/3, pp. 95-120, 1988.
[9] N. Dershowitz,The Evolution of Programs. Boston, MA: Birkhäuser, 1983.
[10] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[11] E. Eder, "Properties of substitutions and unifications,"J. Symbolic Comput., vol. 1, pp. 31-46, 1985.
[12] M. Fay, "First-order unification in an equational theory," inProc. 4th Conf. on Auto. Deduction, 1979, pp. 161-167.
[13] A. Felty and D. Miller, "Specifying theorem provers in a higher-order logic programming language," inProc. 9th Int. Conf. on Auto. Deduction, 1988, pp. 61-80.
[14] M. J. Gordon, A. J. Milner, and C.P. Wadsworth,Edinburgh LCF: A Mechanised Logic of Computation. Berlin: Springer-Verlag, 1979.
[15] J. V. Guttag and J. J. Horning, "Formal specification as a design tool," inProc. 7th ACM Symp. Principles of Programming Languages, 1980, pp. 251-261.
[16] P. Harrison and H. Khoshnevisan, "Efficient compilation of linear recursive functions into object-level loops," inProc. SIGPLAN '86 Sym. on Compiler Constructions, 1986, pp. 207-218.
[17] S. Hayashi and H. Nakano,PX: A Computational Logic. Cambridge, MA: MIT Press, 1988.
[18] L. Hines, "Str+ve ??: the Str+ve based subset prover," inProc. 10th Int. Conf. on Auto. Deduction, 1990, pp. 193-206.
[19] D. Kapur and P. Narendran, "An equational approach to theorem proving in the first-order predicate calculus,"Proc. 9th Int. Joint Conf. on Art. Intell., 1985, pp. 1146-1153.
[20] R. Kowalski, "Predicate logic as a programming language," inProc. IFIP Congress '74, pp. 569-544.
[21] W. W. McCune, "OTTER 2.0 users' guide," Math. and Comput. Sci. Div., Argonne Natl. Lab., 1990.
[22] Z. Manna, M. Stickel, and R. Waldinger, "Monotonicity properties in automated deduction," inArtificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz, Ed. New York: Academic, 1991, pp. 261-280.
[23] Manna, Z., and R. Waldinger, "A Deductive Approach to Program Synthesis,"Trans. Programming Languages and Systems, Vol. 2, No. 1, Jan. 1980, pp. 90-121.
[24] Z. Manna and R. Waldinger, "Deductive synthesis of the unification algorithm,"Sci. Comput. Program., vol. 1, pp. 5-48, 1981.
[25] Z. Manna and R. Waldinger,The Logical Basis for Computer Programming, vol. 1,Deductive Reasoning. Reading, MA: Addison-Wesley, 1985.
[26] Z. Manna and R. Waldinger, "Special relations in automated deduction,"J. ACM, vol. 33, no. 1, pp. 1-59, 1986.
[27] Z. Manna and R. Waldinger, "The origin of a binary-search paradigm,"Sci. Comput. Program., vol. 9, pp. 37-83, 1987.
[28] Z. Manna and R. Waldinger, "The deductive synthesis of imperative LISP programs," inProc 6th AAAI Nat. Conf. on Art. Intell., 1987, pp. 155-160.
[29] Z. Manna and R. Waldinger,The Logical Basis for Computer Programming, vol. 2,Deductive Systems. Reading, MA: Addison-Wesley, 1990.
[30] P. Martin-Löf, "Constructive mathematics and computer programming," inProc. 6th Int. Cong. for Logic, Method., and Phil. of Sci., 1982, pp. 153-175.
[31] N. Murray, "Completely nonclausal theorem proving,"Art. Intell., vol. 18, no. 1, pp. 67-85, 1982.
[32] D. Nardi, "Formal synthesis of a unification algorithm by the deductivetableau method,"J. Logic Program., vol. 7, pp. 1-43, 1989.
[33] B. Nordström, K. Petersson, and J. M. Smith,Programming in Martin-Löf's Type Theory: An Introduction. New York: Oxford Univ. Press, 1990.
[34] L. C. Paulson, "The foundations of a generic theorem prover,"J. Auto. Reasoning, vol. 5, pp. 363-397, 1989.
[35] A. Pnueli and R. Rosner, "A framework for the synthesis of reactive modules," inProc. Concurency '88, 1988, pp. 4-17.
[36] J. A. Robinson, "A machined-oriented logic based on the resolution principle,"J. Assoc. Comput. Mach., vol. 12, no. 1, pp. 23-41, Jan. 1965.
[37] M. Sato, "Towards a mathematical theory of program synthesis," inProc. 6th Int. Joint Conf. on Art. Intell., 1979, pp. 757-762.
[38] M. Schmidt-Schauss, "Computational aspects of an order sorted logic with term declarations," Universität Kaiserslautern, SEKI Rep. SR- 88-10, 1988.
[39] J. Siekmann, "Unification theory,"J. Symbolic Comput., vol. 7, nos. 3/4, pp. 207-274, 1989.
[40] D. R. Smith, "Top-down synthesis of divide-and-conquer algorithms,"Artificial Intell., vol. 27, no. 1, pp. 43-96, Sept. 1985; reprinted inReadings in Artificial Intelligence and Software Engineering, C. Rich and R. Waters, Eds. Los Altos, CA: Morgan Kaufmann, 1986.
[41] N. Shankar, "Checking the proof of Gödel's incompleteness theorem," Instit. Comput. Sci., Univ. Texas at Austin, 1985.
[42] E. Shapiro,Algorithmic Program Debugging. Cambridge, MA: MIT Press, 1983.
[43] M. E. Stickel, "A unification algorithm for associative-commutative functions,"J. ACM, vol. 28, no. 3, pp. 423-434, 1981.
[44] M.E. Stickel, "Automated deduction by theory resolution,"J. Auto. Reason., vol. 1, no. 4, pp. 333-355, 1985.
[45] J. Traugott, "Deductive synthesis of sorting programs,"J. Symbolic Comput., vol. 7, pp. 533-572, 1989.
[46] L. Wos and G. Robinson, "Paramodulation and theorem proving in first-order theories with equality," inMachine Intelligence 4, B. Meltzer and D. Michie, Eds. New York: Elsevier, 1969, pp. 135-150.
[47] L. Wos and S. Winkler, "Open questions solved with the assistance of AURA," inAutomated Theorem Proving: After 25 Years, W. W. Bledsoe and D. W. Loveland, Eds. Providence, RI: Ameri. Math. Soc., 1983, pp. 73-88.

Index Terms:
deductive program synthesis; specification; proof; deductive-tableau system; theorem-proving framework; nonclausal resolution rule; reasoning; induction rule; artificial intelligence; formal specification; inference mechanisms; program testing; theorem proving
Citation:
Z. Manna, R. Waldinger, "Fundamentals of Deductive Program Synthesis," IEEE Transactions on Software Engineering, vol. 18, no. 8, pp. 674-704, Aug. 1992, doi:10.1109/32.153379
Usage of this product signifies your acceptance of the Terms of Use.