  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 refinement. Contextual refinement simplifies the
refinement process by abstractly capturing the context of a subcomponent of a
program, which typically includes information about the values of the free
variables. This paper also extends and generalises module refinement. A module
is a collection of procedures that operate on a common data type; module
refinement between a specification module A and an implementation module C
allows calls to the procedures of A to be systematically replaced with calls to
the corresponding procedures of C. Based on the conditions for module
refinement, we present a method for calculating an implementation module from a
specification module. Both contextual and module refinement within the
refinement calculus have been generalised from earlier work and the results are
presented in a unified framework.
