Where academic tradition
meets the exciting future

Towards a Refinement Algebra

Joakim von Wright, Towards a Refinement Algebra. Science of Computer Programming 51(1-2), 23–45, 2004.


Kleene Algebra with Tests (KAT) has proved to be useful for reasoning
about programs in a partial correctness framework. We describe Demonic
Refinement Algebra (DRA), a variation of KAT for total correctness and
illustrate its modeling and reasoning power with a number of
applications and examples.

BibTeX entry:

  title = {Towards a Refinement Algebra},
  author = {Wright, Joakim von},
  journal = {Science of Computer Programming},
  volume = {51},
  number = {1-2},
  pages = {23–45},
  year = {2004},
  keywords = {Kleene algebra; Refinement; Predicate transformers; Iteration},

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab

Publication Forum rating of this publication: level 2

Edit publication