The Linear Algebra of UTP (Revised Version)
B. Möller
2006-10
Technical Report, Institute of Computer Science, University of Augsburg, April 2006
Abstract:
We show that the well-known algebra of matrices over a semiring can be
used to reason conveniently about predicates as used in the Unifying
Theories of Programming. This allows a simplified treatment
of the designs of Hoare and He and the prescriptions of Dunne. In
addition we connect the matrix approach with the theory of test and
condition semirings and the modal operators diamond and box. In
particular, we show that matrices of predicate transformers allow an
even more streamlined treatment and removal of a restricting
assumption on the underlying semirings.
Downloads:
This page in English
Suche