Normal forms in total correctness for while programs and action systems
2011 (English)In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 80, no 6, 362-375 p.Article in journal (Refereed) Published
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.
Place, publisher, year, edition, pages
2011. Vol. 80, no 6, 362-375 p.
IdentifiersURN: urn:nbn:se:uu:diva-156229DOI: 10.1016/j.jlap.2011.04.008ISI: 000292228200007OAI: oai:DiVA.org:uu-156229DiVA: diva2:431433