Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 |
| Pages | 71-78 |
| Number of pages | 8 |
| DOIs | |
| Publication status | Published - 30 Oct 2013 |
| Event | 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 - Birmingham, United Kingdom Duration: 1 Jul 2013 → 3 Jul 2013 |
Conference
| Conference | 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 |
|---|---|
| Country/Territory | United Kingdom |
| City | Birmingham |
| Period | 1/07/13 → 3/07/13 |