Calculating modules in contextual logic program refinement

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. In this paper we extend and generalise earlier work on contextual and module refinement of logic programs within the refinement calculus, and present the results in a framework. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program; such context typically includes information about the value of the free variables. A module is a collection of procedures that operate on a common data type; module refinement is a condition between specification/implementation modules that determines when calls to the implementation module may (systematically) replace calls to the specification module. Based on the conditions for module refinement, we present a method for ...

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Robert Colvin, Ian J. Hayes, Paul A. Strooper
• Keywords: CORR 2006, Education, Logic Programs, Module Refinement, Specification