Don't Care Non-determinism in Logic Program Refinement
David Hemer, Robert J. Colvin, Ian J. Hayes, Paul A. Strooper · Electronic Notes in Theoretical Computer Science · 2002
The refinement calculus for logic programs consists of a wide-spectrum language and a notion of refinement that can be used to develop programs from specifications. In a refinement, the refined program must return the same set of answers as the original program, because the meaning of a logic program is defined in terms of all the answers computed by the program. “Don't know” non-determinism is supported in the language by allowing more than one answer. In the traditional refinement calculus for imperative programs, there is another form of non-determinism, called “don't care” (or demonic) non-determinism, which allows non-determinism to be eliminated during refinement. Thus, non-deterministic specifications can be refined to deterministic implementations. In this paper, we introduce a notion of don't care non-determinism into the refinement calculus for logic programs. We extend the wide-spectrum language to include non-deterministic choice operators. We present examples that illustrate the use of these operators and describe the changes to the semantics and refinement.