• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Interpreting Nondeterminism in the Refinement Calculus

Ralph-Johan Back, Joakim von Wright, Interpreting Nondeterminism in the Refinement Calculus. In: Proceedings of the 7th Refinement Workshop, Springer-Verlag, 1996.

Abstract:

We introduce a simple programming language and define its
predicate
transformer semantics. We motivate the choice of the constructs for
the language by algebraic arguments, showing that the constructs
are essentially the basic algebraic operations that are available
for predicate transformers, when these are viewed as forming a complete
lattice enriched category. We then show that the statements in the
language can be given a simple operational interpretation, as describing
the interaction between a user and a computing system. This gives
a general intuitive interpretation of angelic and demonic nondeterminism.
We also consider the notion of correctness and refinement of program
statements that this intuitive interpretation gives rise to, and
show the connection between the user-system interpretation and the
interpretation of program execution as a game.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{pBaWri96,
  title = {Interpreting Nondeterminism in the Refinement Calculus},
  booktitle = {Proceedings of the 7th Refinement Workshop},
  author = {Back, Ralph-Johan and Wright, Joakim von},
  publisher = {Springer-Verlag},
  year = {1996},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication