Modal Design Algebra

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

Abstract:
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.

Downloads:

• Modal Design Algebra  -  (tr-2005-15_moe.pdf, 610 KB)