International Journal of Mathematics and Mathematical Sciences
Volume 2004 (2004), Issue 3, Pages 135-160

Demonic semantics: using monotypes and residuals

F. Tchier

Mathematics Department, King Saud University, P.O. Box 22452, Riyadh 11495, Saudi Arabia

Received 13 April 2002

Copyright © 2004 F. Tchier. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.


Relations and relational operators can be used to define the semantics of programming languages. The operations and serve to give angelic semantics by defining a program to go right when there is a possibility to go right. On the other hand, the demonic operations and do the opposite: if there is a possibility to go wrong, a program whose semantics is given by these operators will go wrong; it is the demonic semantics. This type of semantics is known at least since Dijkstra's introduction of the language of guarded commands. Recently, there has been a growing interest in demonic relational semantics of sequential programs. Usually, a construct is given an ad hoc semantic definition based on an intuitive understanding of its behavior. In this note, we show how the notion of relational flow diagram (essentially a matrix whose entries are relations on the set of states of the program), introduced by Schmidt, can be used to give a single demonic definition for a wide range of programming constructs. This research had originally been carried out by J. Desharnais and F. Tchier (1996) in the same framework of the binary homogeneous relations. We show that all the results can be generalized by using the monotypes and the residuals introduced by Desharnais et al. (2000).