Abstract
After an overview on several improvements in the synthesis of functional programs from predicate logic specifications, the sorted narrowing approach is presented in more detail: A sort discipline is introduced to describe regular sets of ground constructor terms as extensional sorts. It is extended to cope with regular sets of ground substitutions, thereby allowing to compute different sorts for terms with different variable bindings. An algorithm to compute signatures of equationally defined functions is sketched that allows potentially infinite overloading. As an application, it is shown how the sort discipline can be used to select solution constructors in narrowing, and hence cuts down the search space of program synthesis drastically.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Oliver Bittel. Ein tableau-basierter Theorembeweiser für die intuitionistische Logik. PhD thesis, Univ. Karlsruhe, 1991.
Jochen Burghardt. Eine feinkörnige Sortendisziplin und ihre Anwendung in der Programmkonstruktion. PhD thesis, Univ. Karlsruhe, 1993.
Jochen Burghardt. The deductive synthesis approach applied to a production cell. In T. Lindner and C. Lewerentz, editors, Formal development of reactive systems — Case study production cell, volume 1 of FZI-Report. FZI Karlsruhe, 1994.
Jochen Burghardt. Deductive synthesis applied to the case study production cell. In T. Lindner and C. Lewerentz, editors, Formal development of reactive systems — Case study production cell, volume 891 of LNCS, pages 297–311. Springer, 1995.
Jochen Burghardt. Regular substitution sets: A means of controlling E-unification. In Proc. Conf. on Rewriting Techniques and Applications, volume 914 of LNCS, pages 382–396, 1995.
Hubert Comon. Equational formulas in order-sorted algebras. In Proc. ICALP, 1990.
Oliver Haase. Nicht-Klausel-Resolution bei der deduktiven Programmsynthese. Master's thesis, University Karlsruhe, 1992.
Birgit Heinz. Lemma discovery by anti-unification of regular sorts. Technical Report 94-21, TU Berlin, 1994.
S. Hölldobler. Foundations of Equational Programming, volume 353 of LNAI. Springer, 1989.
Eduard Klein and M. Martin. The parser generating system PGS. Software Practice and Experience, 19(11):1015–1028, 1989.
Ursula Mohaupt. Deduktive Programmsynthese. Master's thesis, Technical University Berlin, 1991.
U.R. Schmerl. Resolution on formula-trees. Acta Informatica, 25:425–438, 1988.
Manfred Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations. PhD thesis, Univ. Kaiserslautern, Apr 1988.
J.W. Thatcher and J.B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1), 1968.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Burghardt, J. (1995). A fine-grain sort discipline and its application to formal program construction. In: Broy, M., Jähnichen, S. (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, vol 1009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015462
Download citation
DOI: https://doi.org/10.1007/BFb0015462
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60589-8
Online ISBN: 978-3-540-47802-7
eBook Packages: Springer Book Archive