×

Synthesis of programs in computational logic. (English) Zbl 1080.68562

Bruynooghe, Maurice (ed.) et al., Program development in computational logic. A decade of research advances in logic-based program development. Berlin: Springer (ISBN 3-540-22152-2/pbk). Lecture Notes in Computer Science 3049, 30-65 (2004).
Summary: Since the early days of programming and automated reasoning, researchers have developed methods for systematically constructing programs from their specifications. Especially the last decade has seen a flurry of activities including the advent of specialized conferences, such as LOPSTR, covering the synthesis of programs in computational logic. In this paper we analyze and compare three state-of-the-art methods for synthesizing recursive programs in computational logic. The three approaches are constructive/deductive synthesis, schema-guided synthesis, and inductive synthesis. Our comparison is carried out in a systematic way where, for each approach, we describe the key ideas and synthesize a common running example. In doing so, we explore the synergies between the approaches, which we believe are necessary in order to achieve progress over the next decade in this field.
For the entire collection see [Zbl 1051.68004].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

LCF
PDFBibTeX XMLCite
Full Text: DOI