| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 431292 | The Journal of Logic and Algebraic Programming | 2011 | 14 Pages |
Abstract
A classical while-program normal-form theorem is derived in demonic refinement algebra. In contrast to Kozen’s partial-correctness proof of the theorem in Kleene algebra with tests, the derivation in demonic refinement algebra provides a proof that the theorem holds in total correctness. A normal form for action systems is also discussed.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
