By the same authors

Designs with angelic nondeterminism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published copy (DOI)



Publication details

Title of host publicationProceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
DatePublished - 30 Oct 2013
Number of pages8
Original languageEnglish


Hoare and He's Unifying Theories of Programming (UTP) are a predicative relational framework for the definition and combination of refinement languages for a variety of programming paradigms. Previous work has defined a theory for angelic nondeterminism in the UTP; this is basically an encoding of binary multirelations in a predicative model. In the UTP a theory of designs (pre and postcondition pairs) provides, not only a model of terminating programs, but also a stepping stone to define a theory for state-rich reactive processes. In this paper, we cast the angelic nondeterminism theory of the UTP as a theory of designs with the long-term objective of providing a model for well established refinement process algebras like Communicating Sequential Processes (CSP) and Circus.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations