Refinement and Demonic Semantics

  • Jules Desharnais
  • Ali Mili
  • Thanh Tung Nguyen
Part of the Advances in Computing Sciences book series (ACS)


In Chapter 8, it was shown how functional programs can be regarded as elements of a relation algebra. In this chapter, we consider imperative programs, which we view as computing an input-output relation on a set of states. We are interested here in programs that are meant to terminate, not in reactive programs. Our programming language is Dijkstra’s language of guarded commands [Dijkstra 1976], which allows the expression of nondeterminism, thus making a relational approach very natural.


Relation Algebra Partial Identity Loop Body Domain Element Infinite Path 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    The first and second authors acknowledge the financial support of the NSERC (Natural Sciences and Engineering Research Council) of Canada.Google Scholar
  2. 2.
    As in Chapt. 8, the symbol D is used to remind of the qualificative demonic.Google Scholar

Copyright information

© Springer-Verlag Wien 1997

Authors and Affiliations

  • Jules Desharnais
  • Ali Mili
  • Thanh Tung Nguyen

There are no affiliations available

Personalised recommendations