An Abstract Formalisation of Correct Schemas for Program Synthesis

Pierre Flener
Department of Information Science, Uppsala University
Box 513, S-751 20 Uppsala, Sweden
pierre.flener@dis.uu.se

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Manchester M13 9PL, U.K.
kung-kiu@cs.man.ac.uk

Mario Ornaghi
Dipartimento di Scienze dell'Informazione, Universita' degli studi di Milano
Via Comelico 39/41, 20135 Milano, Italy
ornaghi@dsi.unimi.it

Julian Richardson
Mathematical Reasoning Group, Division of Informatics
The University of Edinburgh, 80 South Bridge, Edinburgh EH1 1HN, U.K.
julianr@dai.ed.ac.uk

Abstract:
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, viz. a template T, and a semantic part.
Template T is formalised as an open (first-order) logic program in
the context of the problem domain, characterised as a first-order
axiomatisation, called a specification framework F, 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.