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.
|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|
Author can archive post-print (ie final draft post-refereeing).