Skip to main content
Kent Academic Repository

Angelic Nondeterminism and Unifying Theories of Programming

Cavalcanti, Ana L. C. and Woodcock, Jim (2004) Angelic Nondeterminism and Unifying Theories of Programming. Technical report. University of Kent (KAR id:14151)

Abstract

Hoare and He have proposed unifying theories of programming (UTP): a model of alphabetised relations expressed as predicates, which provides support for program development in a number of programming paradigms. Their objective is the unification of languages and techniques, so that developers can benefit from results of works that were, until then, conflicting in their approach. They consider fundamental programming concepts like nondeterminism, specification as pre and post condition pairs, and concurrency; however, they leave the study of many constructs open. In this report, we investigate the possibility of unifying angelic nondeterminism into the UTP. We consider its general relational setting, and the more restricted setting of designs, which is the basis for all the models considered by Hoare and He. We study isomorphic models based on relations between sets of states and on predicate transformers. We conclude that the introduction of angelic nondeterminism requires a more elaborate relational framework. We proceed to 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.

Item Type: Reports and Papers (Technical report)
Uncontrolled keywords: semantics, refinement, relations, predicate
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/14151 (The current URI for this page, for reference purposes)

University of Kent Author Information

Cavalcanti, Ana L. C..

Creator's ORCID:
CReDIT Contributor Roles:

Woodcock, Jim.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.