Angelic nondeterminism in the unifying theories of programming

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

Research output: Contribution to journalArticle

110 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 languageEnglish
Pages (from-to)288-307
JournalFormal Aspects of Computing
Volume18
Issue number3
DOIs
Publication statusPublished - Sep 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]

Fingerprint Dive into the research topics of 'Angelic nondeterminism in the unifying theories of programming'. Together they form a unique fingerprint.

  • Cite this

    Cavalcanti, A. A., Woodcock, J. C. P. J., & Dunne, S. E. S. (2006). Angelic nondeterminism in the unifying theories of programming. Formal Aspects of Computing, 18(3), 288-307. https://doi.org/10.1007/s00165-006-0001-8