Refining logic programs using types and invariants
Robert J. Colvin, Ian J. Hayes, Paul A. Strooper · 1999
The logic programming refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we show how types, and their generalisation, invariants, which allow conditions that relate several variables, can be handled in the logic programming refinement calculus. Types and invariants provide useful information to both the specifier and the refiner. Two kinds of invariant, one conjoined in parallel and one conjoined sequentially to a program, are discussed. The typical situations where each type of invariant is applicable are discussed and illustrated with examples.