Padawitz P. Deduction and Declarative Programming

Издательство Cambridge University Press, 1992, -285 pp.This monograph promotes specification and programming on the basis of Horn logic with equality. As was pointed out in [Pad88a], this theoretical background equips us with a number of deductive methods for reasoning about specifications and designing correct programs. The term declarative programming stands for the combination of functional (or applicative) and relational (or logic) programming. This does not rule out the design of imperative programs with conditionals, loops and sequences of variable assignments, since all these features have functional or relational equivalents. In particular, variables become "output parameters" of functions. Hence the static view of declarative programming is not really a restriction. Only if correctness conditions concerned with liveness or synchronization are demanded, transition relations must be specified for fixing the dynamics of program execution (cf. Sect. 6.6).Preliminaries
Guards, Generators and Constructors
Models and Correctness
Computing Goal Solutions
Inductive Expansion
Directed Expansion and Reduction
Implications of Ground Confluence
Examples
EXPANDER: Inductive Expansion in SML