Kleene under a Modal Demonic Star

in: Universität Augsburg Technical Report, Institute of Computer Science, University of Augsburg, May 2004

Abstract:
In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalize this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behavior of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalization of the while statement erification rule to nondeterministic loops. The paper generalizes earlier relation-algebraic work to the setting of modal Kleene algebra, an extension of Kozen's Kleene algebra with tests that allows the internalization of weakest liberal precondition and strongest liberal postcondition operators.

Downloads:

• Kleene under a Modal Demonic Star  -  (tr-2004-11_moe.pdf, 747 KB)