TY - GEN
T1 - Unifying Theories of Programming that distinguish nontermination and abort
AU - Hayes, Ian J.
AU - Dunne, Steve E.
AU - Meinicke, Larissa
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=78049436425&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-13321-3_12
DO - 10.1007/978-3-642-13321-3_12
M3 - Conference proceeding contribution
AN - SCOPUS:78049436425
SN - 3642133207
SN - 9783642133206
VL - 6120 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 178
EP - 194
BT - Mathematics of Program Construction - 10th International Conference, MPC 2010, Proceedings
T2 - 10th International Conference on the Mathematics of Program Construction, MPC 2010
Y2 - 21 June 2010 through 23 June 2010
ER -