Demonic semantics: using monotypes and residuals

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).