Fulltext

In praise of algebra

Hoare, Tony ; van Staden, Stephan

In: Formal Aspects of Computing, 2012, vol. 24, no. 4-6, p. 423-431

Ajouter à la liste personnelle
    Titre
    • In praise of algebra
    Auteur
    • Hoare, Tony. Microsoft Research, Cambridge, UK
    • van Staden, Stephan. ETH Zurich, Zurich, Switzerland
    Type de document
    • Postprint
    Langue
    • Anglais
    Publié dans
    • Formal Aspects of Computing, 2012, vol. 24, no. 4-6, p. 423-431. Springer-Verlag
    Autre version électronique
    Identifiant OAI-PMH
    • oai:doc.rero.ch:314341
    Summary
    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