Abstract
The automatic synthesis of program methods [Manna & Waldinger, 1980; Kodratoff & Picard, 1983; Franova, 1985],..., etc, allow an automatic generation of programs from their specifications. As interesting as it is, this approach comes up against a usual problem: to define a good specification is very difficult in itself.
In this paper, we propose a method for developing a specification from a program.
We suppose that the program to transform is recursive and that it is given under the form of rewrite rules. Calls to sub-programs are allowed.
This method aims at the construction of the formal specification of the algorithm implemented by the program
The obtained specification expresses the relations between the inputs and outputs of the program.
In the PROLOG case, the program one starts from is a PROLOG program in which the inputs and outputs are singled out (i.e., a “functional” PROLOG program).
The specification one obtains is a PROLOG program in which the relations between variables are the only significant feature (i.e., a “pure” PROLOG program).
Our method uses the algebraic abstract data types [Bidoit, 1982], rewriting systems [Dershowitz, 1984] and Knuth-Bendix completion algorithm [Knuth & Bendix, 1969] and needs for a theorem prover.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bidoit, M. (1982): Une Mèthode de Prèsentation des Types Abstraits : Applications, Thése 3eme cycie, Universitè de Paris-Sud, Orsay, France, 1982.
Billaud, M. (1985): Une Formalisation des Structures de Contrôle de PROLOG, Thèse de Docteur en Informatique, Université de Bordeaux I, Jan 1985.
Clocksin, W. F., Mellish, C. S. (1984): Programming in PROLOG, Springer-Verlag Berlin Heidelberg New York Tokyo, Second Edition 1984.
Dershowitz, N. (1984): Equations as programming Language, Proceedings Jerusalem Conference on Information Technology, May 1984, Jerusalem, Israel, pp. 114–124.
Floyd, R. W. (1967): Assigning Meaning to Programs, Proc. Symp. in Applied Mathematics, V 19, 1967, pp. 19–32.
Franova, M. (1985): CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs, in: Joshi, A. (ed.), Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, August 1985, pp. 1214–1220
Hoare, C. A. R. (1969): An Axiomatic Basis for Computer Programming, CACM V12, # 10, October 1969, pp. 576–583.
Knuth, D. E., Bendix P. B. (1969): Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, Ed. J. Leech, Pergamon Press, Oxford, pp. 263–297, 1969.
Kodratoff, Y., Picard, M. (1983): Complétion de Systèmes de Réécriture et Synthèse de programmes à partir de leurs spécifications, in: Actes des journées Bigre, France, Cap-d’Adge, October 1983, pp. 68–83
Manna, Z., Waldinger, R. (1980): A Deductive Approach to Program Synthesis in: ACM TOPLAS, V 2, # 1, January 1980, pp. 90–121.
Tareb, N., Kodratoff, Y. (1987): Synthèse de Spécifications à partir de Programmes, Proc. of Séminaire sur la Programmation Logique, Lannion, 19–21 May 1987, pp. 265–283.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tareb, N., Kodratoff, Y. (1987). Synthesis of Specifications from Programs. In: Buchberger, E., Retti, J. (eds) 3. Österreichische Artificial-Intelligence-Tagung. Informatik-Fachberichte, vol 151. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-46620-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-46620-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-18384-6
Online ISBN: 978-3-642-46620-5
eBook Packages: Springer Book Archive