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 th...
Saved in:
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2004-01-01
|
| Series: | International Journal of Mathematics and Mathematical Sciences |
| Online Access: | http://dx.doi.org/10.1155/S016117120420415X |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | 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). |
|---|---|
| ISSN: | 0161-1712 1687-0425 |