Interpreting Nondeterminism in the Refinement Calculus

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.

Conference

Publication date: July 1996

Publication date (Print): July 1996

Pages: 1-11

Affiliations

Department of Computer Science, Abo Akademi University

Turku, Finland

Article

DOI: 10.14236/ewic/RW1996.1

Copyright statement: © Ralph-Johan Back et al. Published by BCS Learning and Development Ltd. Proceedings of the BCS-FACS 7th Refinement Workshop, Bath

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Proceedings of the BCS-FACS 7th Refinement Workshop

Conference acronym: RW

Conference number: 7

Conference location: Bath

Conference date: 3-5 July 1996

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: BCS-FACS 7th Refinement Workshop

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/RW1996.1

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing