Reasoning about loops in total and general correctness

Dunne, Steve E., Hayes, Ian J. and Galloway, Andy J. (2010). Reasoning about loops in total and general correctness. In: Andrew Butterfield, UTP 2008: Revised Selected Papers. Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, (62-81). 8-10 September, 2008. doi:10.1007/978-3-642-14521-6_5

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Dunne, Steve E.
Hayes, Ian J.
Galloway, Andy J.
Title of paper Reasoning about loops in total and general correctness
Conference name Unifying Theories of Programming: Second International Symposium, UTP 2008
Conference location Dublin, Ireland
Conference dates 8-10 September, 2008
Proceedings title UTP 2008: Revised Selected Papers   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2010
Sub-type Fully published paper
DOI 10.1007/978-3-642-14521-6_5
ISBN 978-3-642-14520-9
ISSN 0302-9743
1611-3349
Editor Andrew Butterfield
Volume 5713
Start page 62
End page 81
Total pages 10
Language eng
Abstract/Summary We introduce a calculus for reasoning about programs in total correctness which blends UTP designs with von Wright’s notion of a demonic refinement algebra. We demonstrate its utility in verifying the familiar loop-invariant rule for refining 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 nontermination to be specified 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 refinement algebra. We formulate a loop-invariant rule for refining a general-correctness specification by a while loop, and we use our general-correctness calculus to verify the new rule.
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 4 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 4 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 08 Feb 2011, 13:47:56 EST by Ian Hayes on behalf of School of Information Technol and Elec Engineering