We introduce a calculus for reasoning about programs in total correctness which blends UTP designs with von Wright's notion of a demonic renement algebra. We demonstrate its utility in verifying the familiar loop-invariant rule for rening a total-correctness specification by a while loop. Total correctness equates non-termination with completely chaotic behaviour, with the consequence that any situation which admits non-termination must also admit arbitrary terminating behaviour. General correctness is more discriminating in allowing non termination to be specied together with more particular terminating behaviour. We therefore introduce an analogous calculus for reasoning about programs in general correctness which blends UTP prescriptions with a demonic renement algebra. We formulate a loop-invariant rule for rening a general-correctness specication by a while loop, and we use our general-correctness calculus to verify the new rule.
|Title of host publication||Unifying theories of programming|
|Place of Publication||Heidelberg|
|Publication status||Published - 2010|
|Event||2nd International Symposium on Unifying Theories of Programming - Dublin, Ireland|
Duration: 8 Sep 2008 → 10 Sep 2008
|Name||Unifying Theories of Programming|
|Conference||2nd International Symposium on Unifying Theories of Programming|
|Abbreviated title||UTP 2008|
|Period||8/09/08 → 10/09/08|
Bibliographical noteAuthor can archive post-print (ie final draft post-refereeing).
Dunne, S. E., Hayes, I. J., & Galloway, A. J. (2010). Reasoning about Loops in Total and General Correctness. In Unifying theories of programming (pp. 62-81). (Unifying Theories of Programming; Vol. 5713). Springer-Verlag. https://doi.org/10.1007/978-3-642-14521-6_5