A Formal Approach to Deductive Synthesis of Constraint Logic Programs
Kung-kiu Lau, Mario Ornaghi · The MIT Press eBooks · 1995
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. 1 Introduction Program synthesis is concerned with deriving programs that are correct wrt their specifications. A formal approach to synthesis guarantees ...