Reasoning about Loops in Total and General Correctness

Steve E. Dunne, Ian J. Hayes, Andy J. Galloway

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationUnifying theories of programming
Place of PublicationHeidelberg
PublisherSpringer-Verlag
Pages62-81
DOIs
Publication statusPublished - 2010
Externally publishedYes
Event2nd International Symposium on Unifying Theories of Programming - Dublin, Ireland
Duration: 8 Sep 200810 Sep 2008

Publication series

NameUnifying Theories of Programming
Volume5713
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Symposium on Unifying Theories of Programming
Abbreviated titleUTP 2008
CountryIreland
CityDublin
Period8/09/0810/09/08

Bibliographical note

Author can archive post-print (ie final draft post-refereeing).

Fingerprint Dive into the research topics of 'Reasoning about Loops in Total and General Correctness'. Together they form a unique fingerprint.

  • Cite this

    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