Unifying Theories of Programming that distinguish nontermination and abort

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. © 2010 Springer-Verlag Berlin Heidelberg.