ANU: The Australian National University
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [Research] [Teaching] [Publications] [Software] [CV]
_____________________________________________________________________

The Refinement Calculator:
Proof Support for Program Refinement

Reference

Michael Butler, Jim Grundy, Thomas Långbacka, Rimvydas Ruksenas & Joakim von Wright. The Refinement Calculator: Proof Support for Program Refinement. In Groves & Reeves, eds. Formal Methods Pacific'97: Proceedings of FMP'97, Discrete Mathematics and Theoretical Computer Science Series., July 1997, Wellington. Springer-Verlag, Singapore. pages 40-61.

Abstract

We describe the Refinement Calculator, a tool which supports the application of the refinement calculus to program development. The tool uses a general mechanism for transformational reasoning with HOL as the underlying proof system. A graphical user interface provides the user with menus of transformations and the ability to select and focus on subcomponents of a specification using simple mouse operations. The refinement-oriented transformations are illustrated with a case study.

BibTeX

Here is a suitable BibTeX entry:

  @INPROCEEDINGS{Butler:1997:TRC,
    author      = "Michael Butler and Jim Grundy and
                   Thomas L{\aa}ngbacka and
                   Rimvydas Ruk{\v{s}\.{e}}nas and
                   Joakim von Wright",
    title       = "The Refinement Calculator:
                   Proof Support for Program Refinement",
    pages       = "40-61",
    booktitle   = "Formal Methods Pacific'97:
                   Proceedings of FMP'97",
    year        = 1997,
    editor      = "Lindsay Groves and Steve Reeves",
    series      = "Discrete Mathematics and
                   Theoretical Computer Science",
    address     = "Wellington, New Zealand",
    month       = jul,
    year        = 1997,
    publisher   = "Springer-Verlag"}

Where To Find it

If you are having trouble finding the proceedings in which this paper appears, then the following information may be of help:

Title: Formal Methods Pacific'97: Proceedings of FMP'97
Editors: Lindsay Groves and Steve Reeves
Series: Discrete Mathematics & Theoretical Computer Science
Copyright: 1997
Publisher: Springer-Verlag, Singapore
ISBN: 981-3083-31-X
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [Research] [Teaching] [Publications] [Software] [CV]
_____________________________________________________________________
Feedback & Queries: Jim Grundy
Date Last Modified: Thu 11 Nov 1999
Universal Ressource Locator: file:/home/jgrundy/www//Publications/fmp97.html