Abstract
The total correctness of sequential computations can be established through different isomorphic models, such as monotonic predicate transformers and binary multirelations, where both angelic and demonic nondeterminism are captured. Assertional models can also be used to characterise process algebras: in Hoare and He’s Unifying Theories of Programming, CSP processes can be specified as the range of a healthiness condition over designs, which are pre and postcondition pairs. In this context, we have previously developed a theory of angelic designs that is a stepping stone for the natural extension of the concept of angelic nondeterminism to the theory of CSP. In this paper we present an extended model of upward-closed binary multirelations that is isomorphic to angelic designs. This is a richer model than that of standard binary multirelations, in that we admit preconditions that rely on later or final observations as required for a treatment of processes.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Back, R., Wright, J.: Refinement calculus: a systematic introduction. Graduate texts in computer science. Springer (1998)
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)
Martin, C.E., Curtis, S.A., Rewitzky, I.: Modelling Nondeterminism. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 228–251. Springer, Heidelberg (2004)
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)
Ribeiro, P., Cavalcanti, A.: Designs with Angelic Nondeterminism. In: 2013 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 71–78 (2013)
Ribeiro, P.: Designs with Angelic Nondeterminism. Technical report, University of York (February 2013), http://www-users.cs.york.ac.uk/pfr/reports/dac.pdf
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)
Ribeiro, P., Cavalcanti, A.: Angelicism in the Theory of Reactive Processes. In: Unifying Theories of Programming (to appear, 2014)
Cavalcanti, A., Mota, A., Woodcock, J.: Simulink Timed Models for Program Verification. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 82–99. Springer, Heidelberg (2013)
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)
Cavalcanti, A., Woodcock, J.: Angelic Nondeterminism and Unifying Theories of Programming. Technical report, University of Kent (2004)
Morgan, C.: Programming from specifications. Prentice Hall (1994)
Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9, 287–306 (1987)
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(Pt. B), 224–240 (2014); Special Issue on Mathematics of Program Construction (2012)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Ribeiro, P., Cavalcanti, A. (2014). UTP Designs for Binary Multirelations. In: Ciobanu, G., Méry, D. (eds) Theoretical Aspects of Computing – ICTAC 2014. ICTAC 2014. Lecture Notes in Computer Science, vol 8687. Springer, Cham. https://doi.org/10.1007/978-3-319-10882-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-10882-7_23
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10881-0
Online ISBN: 978-3-319-10882-7
eBook Packages: Computer ScienceComputer Science (R0)