A Formal Approach to Deductive Synthesis of Constraint Logic Programs

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, 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:
Formal program synthesis is concerned with deriving programs that
are (formally) correct wrt their specifications, and is therefore
of crucial importance to formal development of verifiably correct
software. Declarative paradigms such as logic programming are 
particularly suitable for program synthesis, and we have formulated a
formal approach to synthesising standard logic programs. Our approach
is object-oriented in the sense that it allows the synthesis of
modular, reusable, and hence maintainable programs. In this paper, we
propose a formal approach to synthesising constraint logic programs
based on our current work. We will show that this approach can be used
to synthesise modular and reusable CLP programs. An integral part of
this paper is the introduction of an abstract semantics to reason
about the synthesis of CLP programs.