@inproceedings{4d0d0801510e472587e5f1a99fd5078a,

title = "Reasoning about Loops in Total and General Correctness",

abstract = "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.",

author = "Dunne, {Steve E.} and Hayes, {Ian J.} and Galloway, {Andy J.}",

note = "Author can archive post-print (ie final draft post-refereeing).; 2nd International Symposium on Unifying Theories of Programming, UTP 2008 ; Conference date: 08-09-2008 Through 10-09-2008",

year = "2010",

doi = "10.1007/978-3-642-14521-6_5",

language = "English",

series = "Unifying Theories of Programming",

publisher = "Springer-Verlag",

pages = "62--81",

booktitle = "Unifying theories of programming",

}