On Correct Program Schemas

Pierre Flener
Department of Computer Science
Bilkent University, 06533 Bilkent, Ankara, Turkey
pf@cs.bilkent.edu.tr

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

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

Abstract:
We present our work on the representation and correctness of
program schemas, in the context of logic program synthesis.
Whereas most researchers represent schemas purely syntactically
as higher-order expressions, we shall express a schema as an open 
first-order theory that axiomatises a problem domain,  called
a specification framework, containing an open program that represents 
the template of the schema. We will show that using our approach we
can define a meaningful notion of correctness for schemas, viz. that
correct program schemas can be expressed as parametric specification 
frameworks containing templates that are steadfast, i.e. programs that
are always correct provided their open relations are computed correctly.