### 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 language | English |
---|---|

Title of host publication | Unifying theories of programming |

Place of Publication | Heidelberg |

Publisher | Springer-Verlag |

Pages | 62-81 |

DOIs | |

Publication status | Published - 2010 |

Externally published | Yes |

Event | 2nd International Symposium on Unifying Theories of Programming - Dublin, Ireland Duration: 8 Sep 2008 → 10 Sep 2008 |

### Publication series

Name | Unifying Theories of Programming |
---|---|

Volume | 5713 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 2nd International Symposium on Unifying Theories of Programming |
---|---|

Abbreviated title | UTP 2008 |

Country | Ireland |

City | Dublin |

Period | 8/09/08 → 10/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