PRECOMAS an implementation of constructive matching methodology

ABSTRACT

The system PRECOMAS (PRoofs Educed by COnstructive MAtching for Synthesis) implements the Constructive Matching methodology for automatic constructions of programs from formal specifications. In this paper we describe briefly the goal of PRECOMAS, its logical background and the CM method applied to proving atomic formulae. We show how the user of our system is involved in solving a program synthesis problem. We show that this interaction does not concern the problem of guiding the program synthesis process, this being solved by CM. Our experimental version serves to confirm that the system is worth to be developed.

REFERENCES

• bibel01: W. Bibel, K. M. Hoemig: LOPS - A System Based on a Strategical Approach to Program Synthesis; {biermann01}, 1984, 69-91.
• biermann01: Alan W. Biermann , Yves Kodratoff , GGerard Guiho, Automatic Program Construction Techniques, The Free Press, New York, NY, 1984
• biundo03: S. Biundo: A synthesis system mechanizing proofs by induction; in: ECAr 86 Proceedings, Vol. 1, 1986, 69-78.
• clark02: K. L. Clark, J. DaHington: Algorithm classification through synthesis; The Computer Journal, Volume 23, Number 1, 6t-65.
• dershowitz03: N. Dershowitz: Synthesis by Completion; {joshi02}, 208-214.
• franova11: M. Franova: An Implementation of Program Synthesis from Formal Specifications; {kodratoff23}, 559-564.
• franova17: M. Franova: Fundamentals of a new methodology for Program Synthesis from Formal Specifications: CM-construction of atomic formulae; Thesis, Universit6 Paris-Sud, November, Orsay, France, 1988.
• franova19: M. Franova: Precomas 0.3 User Guide; Rapport de Recherche No.524, L.R.I., Universit6 de Paris-Sud, Orsay, France, October, 1989.
• franova22: M. Franova: CM Methodology for Equation solving in the program synthesizer PRECOMAS, in preparation.
• joshi02: A.K Joshi, (ed): Proceedings of the Ninth International loint Conference on Artificial Intelligence; August, Los Angeles, 1985.
• kodratoff04: Y. Kodratoff, M.Picard: Compl6tion de syst{mes de r66criture et synth~se de programmes ~ partir de leurs sp6cifications; Bigre No.35, October, 1983.
• kodratoff23: Y. Kodratoff: Proceedings of the 8th European Conference on Artificial Intelligence; August 1-5, Pitman, London, United Kingdom, 1988.
• manna-waldinger01: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• smith03: Douglas R. Smith, Top-down synthesis of divide-and-conquer algorithms, Artificial Intelligence, v.27 n.1, p.43-96, Sept. 1985 [doi>10.1016/0004-3702(85)90083-9]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

General Terms:
Algorithms, Design, Theory