Abstract
In this paper we propose a method for program synthesis from constructive proofs based on a particular proof strategy, we call dischargeable set construction. This proof-strategy allows to build proofs in which active patterns (sequences of application of rules with proper computational content) can be distinguished from correctness patterns (concerning correctness properties of the algorithm implicitly contained in the proof). The synthesis method associates with every active pattern of the proof a program schema (in an imperative language) translating only the computational content of the proof. One of the main features of our method is that it can be applied to a variety of theories formalizing ADT’s and classes of ADT’s. Here we will discuss the method and the computational content of some principles of particular interest in the context of some classes of ADT’s.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Avellone. The algorithmic content of constructive proofs: translating proof s into programs and interpreting proofs as programs. PhD thesis, Dipartimento di Scienze dell’Informazione, Università degli Studi di Milano, Italy, 1998.
J. Bates and R. Constable. Proof as programs. ACM Transaction on Programming Languages and Systems, 7(1):113–136, 1985.
U. Berger and H. Schwichtenberg. The greatest common divisor: A case study for program extraction from classical proofs. Lecture Notes in Computer Science, 1158:36–46, 1996.
A. Bertoni, G. Mauri, and P. Miglioli. On the power of model theory to specify abstract data types and to capture their recursiveness. Fundamenta Informaticae, VI(2):127–170, 1983.
A. Bertoni, G. Mauri, P. Miglioli, and M. Ornaghi. Abstract data types and their extension within a constructive logic. In G. Kahn, D.B. MacQueen, and G. Plotkin, editors, Semantics of data types, LNCS 173, pages 177–195. Springer Verlag, 1984.
A. Bertoni, G. Mauri, P. Miglioli, and M. Wirsing. On different approaches to abstract data types and the existence of recursive models. EATCS bulletin, 9:47–57, 1979.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1. Berlin: Springer-Verlag, 1985.
C.A. Goad. Proofs as description of computation. In CADE 5, pages 39–52. Springer-Verlag, LNCS, 1980.
K.-K. Lau and M. Ornaghi. On specification frameworks and deductive synthesis of logic programs. In Logic Program Synthesis and Transformation. Proceedings of LOPSTR’94, Pisa, Italy, 1994.
K.-K. Lau and M. Ornaghi. Towards an object-oriented methodology for deductive synthesis of logic programs. Lecture Notes in Computer Science, 1048:152–169, 1996.
P. Miglioli, U. Moscato, and M. Ornaghi. Program specification and synthesis in constructive formal systems. In K.-K. Lau and T.P. Clement, editors, Logic Program Synthesis and Transformation, Manchester 1991, pages 13–26. Springer-Verlag, 1991. Workshops in Computing.
P. Miglioli, U. Moscato, and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. Journal of Symbolic Computation, 18:41–81, 1994.
P. Miglioli, U. Moscato, M. Ornaghi and G. Usberti. A constructivism based on classical truth. Notre Dame Journal of Formal Logic, 30(1): 67–90, 1989.
P. Miglioli and M. Ornaghi. A logically justified model of computation. Fundamenta Informaticae, IV,1,2:151–172,277–341, 1981.
C.R. Murthy. Classical proofs as programs: How, what, and why. Lecture Notes in Computer Science, 613:71–88, 1992.
H. Schwichtenberg. Proofs as programs. In P. Aczel, H. Simmons, and S. S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 81–113. Cambridge University Press, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avellone, A., Ferrari, M., Miglioli, P. (1999). Synthesis of Programs in Abstract Data Types. In: Flener, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 1998. Lecture Notes in Computer Science, vol 1559. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48958-4_5
Download citation
DOI: https://doi.org/10.1007/3-540-48958-4_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65765-1
Online ISBN: 978-3-540-48958-0
eBook Packages: Springer Book Archive