Abstract
We survey the well-known algebraic laws of sequential programming, and extend them with some less familiar laws for concurrent programming. We give an algebraic definition of the Hoare triple, and algebraic proofs of all the relevant laws for concurrent separation logic. We give the provable concurrency laws for Milner transitions, for the Back/Morgan refinement calculus, and for Dijkstra’s weakest preconditions. We end with a section in praise of algebra, of which Carroll Morgan is such a master.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Back R-J (1978) On the correctness of refinement steps in program development. PhD thesis, A^bo Akademi, Department of Computer Science. Helsinki, Finland. Report A-1978-4
Back R-J (1979) On the notion of correct refinement of programs. In: 5th Scandinavian logic symposium, Aalborg, Denmark. Aalborg University Press, Denmark
Back R-J (1980) Correctness preserving program refinements: proof theory and applications. Mathematical center tracts, vol 131. Mathematical Centre, Amsterdam
Back R-J (1981) Proving total correctness of nondeterministic programs in infinitary logic. Acta Informatica 15: 233–249
Böhme S, Nipkow T (2010) Sledgehammer: judgement day. In: Proceedings of the 5th international conference on automated reasoning, IJCAR’10. Springer, Berlin, pp 107–121
Dijkstra EW (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs
Foster S, Struth G, Weber T (2011) Automated engineering of relational and algebraic methods in Isabelle/HOL. In: Proceedings of the 12th international conference on relational and algebraic methods in computer science, RAMICS’11. Springer, Berlin, pp 52–67
Hoare CAR, Hayes IJ, Jifeng He, Morgan CC, Roscoe AW, Sanders JW, Sorensen IH, Spivey JM, Sufrin BA (1987) Laws of programming. Commun ACM 30: 672–686
Hoare CAR, Hussain A, Möller B, O’Hearn P, Petersen R, Struth G (2011) On locality and the exchange law for concurrent processes. In: Joost-Pieter K, Barbara König (eds) CONCUR 2011 concurrency theory. Lecture Notes in Computer Science, vol 6901. Springer, Berlin, pp 250–264
Hoare C, Möller B, Struth G, Wehrman I (2009) Concurrent Kleene algebra. In: Mario B, Gianluigi Z (eds) CONCUR 2009—concurrency theory. Lecture Notes in Computer Science, vol 5710. Springer, Berlin, pp 399–414
Hoare T, Möller B, Struth G, Wehrman I (2011) Concurrent Kleene algebra and its foundations. J Logic Algebraic Program, 80(6): 266–296
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12: 576–580
Hoare CAR, Wehrman I, O’Hearn PW (2009) Graphical models of separation logic. In: Manfred B, Wassiou S, Tony H (eds) Proceedings of the 2008 Marktoberdorf Summer School on engineering methods and tools for software safety and security. IOS Press, Amsterdam
Kozen D (1994) A completeness theorem for Kleene algebras and thealgebra of regular events. Inf Comput 110: 366–390
Milner R (1980) A calculus of communicating systems. Lecture Notes in Computer Science, vol 92. Springer, Berlin
Morgan C (1988) The specification statement. ACM Trans Program Lang Syst 10: 403–419
Morgan C (1994) Programming from specifications, 2nd edn. Prentice Hall International (UK) Ltd, Hertfordshire
Nipkow T, Wenzel M, Paulson LC (2002) Isabelle/HOL: a proof assistant for higher-order logic. Springer, Berlin
O’Hearn P (2004) Resources, concurrency and local reasoning. In: Philippa G, Nobuko Y (eds) CONCUR 2004—concurrency theory. Lecture Notes in Computer Science. Springer, Berlin, pp 49–67
O’Hearn PW, Reynolds JC, Yang H (2001) Local reasoning about programs that alter data structures. In: CSL ’01, of LNCS, vol 2142. Springer, Berlin, pp 1–19
Isabelle/HOL (2011) Proofs. http://se.inf.ethz.ch/people/vanstaden/InPraiseOfAlgebra.thy,
Wehrman I, Hoare CAR, O’Hearn PW (2009) Graphical models of separation logic. Inf Process Lett 109(17): 1001–1004
Author information
Authors and Affiliations
Corresponding author
Additional information
Peter Höfner, Robert van Glabbeek and Ian Hayes
Dedication: to Carroll Morgan, whose use of algebra has so often given delight to so many of his audience.
Van Staden was supported by ETH Research Grant ETH-15 10-1.
Rights and permissions
About this article
Cite this article
Hoare, T., van Staden, S. In praise of algebra. Form Asp Comp 24, 423–431 (2012). https://doi.org/10.1007/s00165-012-0249-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-012-0249-0