Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    A Tool for Logic Program Refinement

    2nd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th July 1997


    R. Colvin, I. Hayes, R. Nickson & P. Strooper


    The refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specifications.

    In the original refinement calculus, the target language is an imperative programming language, but more recently a refinement calculus for deriving logic problems has been proposed.

    Due to the amount of detail involved, the manual refinement of programs is a tedious and time-consuming task, and is therefore an obvious candidate for tool support.

    Several tools exist for the imperative refinement calculus, and in this paper we describe a prototype tool to support the recently developed refinement calculus for logic problems. The tool was developed using Ergo, an interactive theorum prover.

    To provide tool support for the calculus, its underlying semantic model was defined within Ergo, and the laws of the calculus were proven in that framework. We illustrate the tool using a simple example refinement.


    PDF filePDF Version of this Paper (217kb)