Unifying Theories of Programming that distinguish nontermination and abort

Ian J. Hayes, Steve E. Dunne, Larissa Meinicke

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

17 Citations (Scopus)

Abstract

In this paper we focus on the relationship between a number of specification models. The models are formulated in the Unifying Theories of Programming of Hoare and He, but correspond to widely used specification models. We cover issues such as partial correctness, total correctness, and general correctness. The properties we use to distinguish the models are these: - whether they allow the specification of assumptions about the initial state outside of which no guarantees are given about the behaviour of the program, i.e., the program may "abort"; - whether a specification may allow or even require nontermination as a valid (non-aborting) outcome; and - whether they allow the expression of tests or enabling conditions, outside of which the program has no possible behaviour. When considering termination, we consider both an abstract model, which only distinguishes whether a program terminates or not, as well as models that include a notion of time: either abstract time representing a notion of progress or real-time.

Original languageEnglish
Title of host publicationMathematics of Program Construction - 10th International Conference, MPC 2010, Proceedings
Pages178-194
Number of pages17
Volume6120 LNCS
DOIs
Publication statusPublished - 2010
Event10th International Conference on the Mathematics of Program Construction, MPC 2010 - Quebec City, QC, Canada
Duration: 21 Jun 201023 Jun 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6120 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other10th International Conference on the Mathematics of Program Construction, MPC 2010
CountryCanada
CityQuebec City, QC
Period21/06/1023/06/10

Fingerprint Dive into the research topics of 'Unifying Theories of Programming that distinguish nontermination and abort'. Together they form a unique fingerprint.

Cite this