An Abstract Formalization of Correct Schemas for Program Synthesis

Pierre Flener, Kung K. Lau, Mario Ornaghi, Julian Richardson

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)


Program schemas should capture not only structured program design principles, but also domain knowledge, both of which are of crucial importance for hierarchical program synthesis. However, most researchers represent schemas as purely syntactic constructs, which can provide only a program template, but not the domain knowledge. In this paper, we take a semantic approach and show that a schema S consists of a syntactic part, namely a template T, and a semantic part. Template T is formalized as an open (first-order) logic program in the context of the problem domain, characterized as a first-order axiomatization, called a specification frameworkF, which is the semantic part. F endows the schema S with a formal semantics, and enables us to define and reason about its correctness. Naturally, correct schemas can be used to guide the synthesis of correct programs. © 2000 Academic Press.

Original languageEnglish
Pages (from-to)93-127
Number of pages35
JournalJournal of Symbolic Computation
Issue number1
Publication statusPublished - Jul 2000


Dive into the research topics of 'An Abstract Formalization of Correct Schemas for Program Synthesis'. Together they form a unique fingerprint.

Cite this