Modal Design Algebra

W. Guttmann, B. Möller

Technical Report, Institute of Computer Science, University of Augsburg, October 2005

We give an algebraic model of (H3) designs of Hoare's and He's Unifying Theories of Programming. It is based on a variant of modal semirings, hence generalizing the original relational model. This makes the theory applicable to a wider class of settings, e.g., to algebras of sets of traces. Moreover, we set up the connection with the weakly and strongly demonic semantics of programs as discussed by a number of authors. This is done using commands (a,t) where a corresponds to the transition relation of a program and the condition t characterizes the input states from which termination is guaranteed. The commands form not only a semiring but even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed point semantics of the demonic while loop.