Angelic Nondeterminism in the Unifying Theories of Programming

TY - JOUR

T1 - Angelic Nondeterminism in the Unifying Theories of Programming

AU - Cavalcanti, A.

AU - Woodcock, J.

AU - Dunne, S.

PY - 2006/9

Y1 - 2006/9

N2 - Hoare and He's unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of Hoare and He's work is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.

AB - Hoare and He's unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of Hoare and He's work is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.

KW - semantics

KW - refinement

KW - relations

KW - predicate transformers

KW - DATA REFINEMENT

U2 - 10.1007/s00165-006-0001-8

DO - 10.1007/s00165-006-0001-8

M3 - Article

SN - 0934-5043

VL - 18

SP - 288

EP - 307

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 3

ER -