Contextual and data refinement for the refinement calculus for logic programs
Robert J. Colvin · The University of Queensland · 2002
The refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. This thesis investigates extensions to the logic programming refinement calculus in the area of contextual refinement, with an emphasis on data refinement. To introduce contextual refinement we examine in detail the semantics of the wide-spectrum language. Refinement laws are developed that simplify the refinement process by handling context implicitly, rather than requiring the context to be explicitly propagated through the program. We use the contextual refinement framework to develop data refinement, where the type representation of a variable is replaced with another. This may be to replace a specification type with an implementation type, or to use a more efficient type. Such refinements take place on a procedure-by-procedure basis, in the context of a coupling invariant, which relates the two types. We then extend data refinement to module refinement, by considering groups of related procedures that share a common data type. By considering the context provided by programs that use a module, we may develop efficient implementations by changing the module's data type.