Abstract
We are developing a shared-variable refinement calculus in the style of the sequential calculi of Back, Morgan, and Morris. As part of this work, we’re studying different theories of shared-variable programming. Using the concepts and notations of Hoare & He’s unifying theories of programming (UTP), we give a formal semantics to a programming language that contains sequential composition, conditional statements, while loops, nested parallel composition, and shared variables. We first give a UTP semantics to labelled action systems, and then use this to give the semantics of our programs. Labelled action systems have a unique normal form that allows a simple formalisation and validation of different logics for reasoning about shared-variable programs. In this paper, we demonstrate how this is done for Lamport’s Concurrent Hoare Logic.
This work has been supported by the QinetiQ grant CU009-019346 on “Advances in formal modelling and concurrency as represented by the Circus language.
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
R-J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proc 2nd Annual Symposium on Principles of Distributed Computing, Montreal, 1983.
R. J. R. Back and J. Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.
Willem-Paul de Roever, Frank S. de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Number 54 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.
C. A. R. Hoare and He Jifeng. Unifying Theories of Programming. Series in Computer Science. Prentice Hall, 1998.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, October 1969.
C. B. Jones. Development methods for computer programs including a notion of interference. PhD thesis, University of Oxford, 1981.
Leslie Lamport and Fred B. Schneider. The ‘Hoare Logic’ of CSP, and All That. ACM Transactions on Programming Languages and Systems, 6(2):281–296, April 1984.
Leslie Lamport. The ‘Hoare Logic’ of Concurrent Programs. Acta Informatica, 14:21–37, 1980.
C. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
J. M. Morris. A Theoretical Basis for Stepwise Refinement and the Programming Calculus. Science of Computer Programming, 9(3):287–306, 1987.
Susan Owicki and David Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319–340, 1976.
Jim Woodcock and Arthur Hughes. Validation of Lamport’s Concurrent Hoare Logic. Technical report, Computing Laboratory, University of Kent, Canterbury, UK, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woodcock, J., Hughes, A. (2002). Unifying Theories of Parallel Programming. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive