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

A Three-Valued Logic for Refinement

Reference

Jim Grundy. A Three-Valued Logic for Refinement. In Bjørner, et.al. (eds). Formal Methods in Programming and Their Applications: Proceedings of the International Conference, volume 735 of Lecture Notes in Computer Science. Novosibirsk, Russia, June 1993. Springer-Verlag. pages 26-42.

Abstract

Predicates are a popular tool for specification. Unfortunately, they are less well suited to defining the semantics of programming languages. As a result, program refinement techniques are usually based on predicate transformers. This paper proposes a three-valued logic with a richer kind of predicate that is suitable for both specification and defining programming language semantics.

The other contribution of this work is a method of refining specifications into recursive programs. It has been suggested that it is more difficult to develop recursive programs than iterative ones. We sidestep the difficulties by using an approximation to the meaning of recursive specifications. We prove that once the refinement process is complete, our approximation is refined by the true meaning.

BibTeX

Here is a suitable BibTeX entry:

  @INPROCEEDINGS{Grundy:1993:TVL,
    author      = "Jim Grundy",
    title       = "A Three-Valued Logic for Refinement",
    pages       = "26-42",
    editor      = "Dines Bj{\o}rner and Manfred Broy and
                   Igor V. Pottosin",
    booktitle   = "Formal Methods in Programming and
                   Their Applications: Proceedings of
                   the International Conference",
    series      = "Lecture Notes in Computer Science",
    volume      = 735,
    address     = "Novosibirsk, Russia",
    month       = jun,
    year        = 1993,
    publisher   = "Springer-Verlag"}

Citations

If you liked this paper, then you might also like the following papers which cite it:

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 in Programming and Their Applications: International Conference
Editors: Dines Bjørner, Manfred Broy and Igor V. Pottosin
Series: Lecture Notes in Computer Science
Volume: 735
Copyright: 1993
Publisher: Springer-Verlag, Berlin, New York
LoC Call #: QA76.6 .F577 1993
LoC Card #: 93-21317
Dewy Call #: 005.1 dc20
ISBN: 3-540-57316-X (Berlin)
0-387-57316-X (New York)
_____________________________________________________________________
[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/fmp93b.html