Note: Most SVRC technical reports are available via anonymous ftp, from svrc.it.uq.edu.au in the directory /pub/techreports. Individual abstracts and compressed postscript les are available from Abstract The reenement calculus provides a method for transforming speciications to executable code, maintaining the correctness of the code with respect to its speciication. In the original reene-ment calculus, the target language is an imperative programming language, but more recently a reenement calculus for deriving logic programs has been proposed. Due to the amount of detail involved, the manual reenement of programs is a tedious and time-consuming task, and is therefore an obvious candidate for tool support. Several tools exist for the imperative reenement calculus, and in this paper we describe a prototype tool to support the recently developed reenement calculus for logic programs. The tool was developed using Ergo, an interactive theorem prover. To provide tool support for the calculus, its underlying semantic model was deened within Ergo, and the laws of the calculus were proven in that framework. We illustrate the tool using a simple example reenement.
分享
引用
