Abstract
The concept of angelic nondeterminism has traditionally been employed in the refinement calculus. Despite different notions having been proposed in the context of process algebras, namely Communicating Sequential Processes (CSP), the analogous counterpart to the angelic choice operator of the monotonic predicate transformers, has been elusive. In order to consider this concept in the context of reactive processes, we introduce a new theory in the setting of Hoare and He’s Unifying Theories of Programming (UTP). Based on a theory of designs with angelic nondeterminism previously developed, we show how these processes can be similarly expressed as reactive designs. Furthermore, a Galois connection is established with the existing theory of reactive processes and a bijection is also found with respect to the subset of non-angelic processes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9, 287–306 (1987)
Morgan, C.: Programming from specifications. Prentice Hall (1994)
Back, R., Wright, J.: Refinement calculus: a systematic introduction. Graduate texts in computer science. Springer (1998)
Tyrrell, M., Morris, J.M., Butterfield, A., Hughes, A.: A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 123–137. Springer, Heidelberg (2006)
Roscoe, A.W.: Understanding concurrent systems. Springer (2010)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)
Cavalcanti, A., Woodcock, J., Dunne, S.: Angelic nondeterminism in the unifying theories of programming. Formal Aspects of Computing 18, 288–307 (2006)
Rewitzky, I.: Binary Multirelations. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 256–271. Springer, Heidelberg (2003)
Ribeiro, P., Cavalcanti, A.: Designs with Angelic Nondeterminism. In: 2013 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 71–78 (2013)
Cavalcanti, A., Woodcock, J.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)
Woodcock, J., Cavalcanti, A.: A Tutorial Introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004)
Ribeiro, P.: Reactive angelic processes. Technical report, University of York (February 2014). http://www-users.cs.york.ac.uk/pfr/reports/rac.pdf
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1998)
Morris, J.M.: Augmenting Types with Unbounded Demonic and Angelic Nondeterminacy. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 274–288. Springer, Heidelberg (2004)
Morris, J.M., Tyrrell, M.: Terms with unbounded demonic and angelic nondeterminacy. Science of Computer Programming 65(2), 159–172 (2007)
Hesselink, W.H.: Alternating states for dual nondeterminism in imperative programming. Theoretical Computer Science 411(22–24), 2317–2330 (2010)
Guttmann, W.: Algebras for correctness of sequential computations. Science of Computer Programming 85, Part B(0), 224–240 (2014). Special Issue on Mathematics of Program Construction 2012
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Ribeiro, P., Cavalcanti, A. (2015). Angelicism in the Theory of Reactive Processes. In: Naumann, D. (eds) Unifying Theories of Programming. UTP 2014. Lecture Notes in Computer Science(), vol 8963. Springer, Cham. https://doi.org/10.1007/978-3-319-14806-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-14806-9_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14805-2
Online ISBN: 978-3-319-14806-9
eBook Packages: Computer ScienceComputer Science (R0)