On Two Dually Nondeterministic Refinement Algebras

in: Universität Augsburg Technical Report, Institute of Computer Science, University of Augsburg, February 2006

Abstract:
A dually nondeterministic refinement algebra with a negation operator is proposed. The algebra facilitates reasoning about total-correctness preserving program transformations and nondeterministic programs. The negation operator is used to express enabledness and termination operators through a useful explicit definition. As a small application, a property of action systems is proved employing the algebra. A dually nondeterministic refinement algebra without the negation operator is also discussed.

Downloads:

• On Two Dually Nondeterministic Refinement Algebras  -  (tr-2006-5_sol.pdf, 212 KB)