Demonic semantics: using monotypes and residuals (Q1774651)

The paper is concerned with the operational and the denotational semantics of nondeterministic programs, and in particular with the so called demonic semantics. While the angelic semantics assumes that if a program has the possibility to go right, it will go right, the demonic semantics assumes that the program will behave as badly as possible. In the operational semantics the behaviour of a program is described by a relation between the initial and final states. In the denotational semantics a mathematical object is associated with a program. In the paper the object is a relational flow diagram whose arrows are weighted by the different steps of the program. The operations are ``demonic choice'' and ``demonic composition''. The notion of relational flow diagram can be used to give a single demonic definition for a wide range of programming constructs. The author shows that for the sequence, Dijkstra's guarded command and the whileloop his definition is equivalent to traditional definitions. The research had originally been carried out in the framework of binary homogeneous relations. Monotypes and residuals used in this paper allow generalizing results obtained previously.