Angelic nondeterminism in the unifying theories of programming

A. (Ana) Cavalcanti; J. C. P. (Jim) Woodcock; S. E. (Steve) Dunne

doi:10.1007/s00165-006-0001-8

Angelic nondeterminism in the unifying theories of programming

A. (Ana) Cavalcanti
, J. C. P. (Jim) Woodcock
, S. E. (Steve) Dunne

Teesside University

Research output: Contribution to journal › Article › peer-review

371 Downloads (Pure)

Abstract

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.

Original language	English
Pages (from-to)	288-307
Journal	Formal Aspects of Computing
Volume	18
Issue number	3
DOIs	https://doi.org/10.1007/s00165-006-0001-8
Publication status	Published - Sept 2006

Bibliographical note

Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 12/11/09]

Access to Document

10.1007/s00165-006-0001-8

PublicationAccepted author manuscript, 208 KBLicence: CC BY-NC-ND

http://hdl.handle.net/10149/58302

Cite this

@article{f73e8c1da9bb4ed183a1753ace713b45,

title = "Angelic nondeterminism in the unifying theories of programming",

abstract = "Hoare and He{\textquoteright}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{\textquoteright}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.",

author = "Cavalcanti, \{A. (Ana)\} and Woodcock, \{J. C. P. (Jim)\} and Dunne, \{S. E. (Steve)\}",

note = " Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 12/11/09]",

year = "2006",

month = sep,

doi = "10.1007/s00165-006-0001-8",

language = "English",

volume = "18",

pages = "288--307",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery",

number = "3",

}

TY - JOUR

T1 - Angelic nondeterminism in the unifying theories of programming

AU - Cavalcanti, A. (Ana)

AU - Woodcock, J. C. P. (Jim)

AU - Dunne, S. E. (Steve)

N1 - Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 12/11/09]

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.

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 -

Angelic nondeterminism in the unifying theories of programming

Abstract

Bibliographical note

Access to Document

Fingerprint

Cite this