Process algebra with guards | SpringerLink
Skip to main content
Springer Nature Link
Log in

Process algebra with guards

Combining hoare logic with process algebra

  • Selected Presentations
  • Conference paper
  • First Online:
CONCUR '91 (CONCUR 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 527))

Included in the following conference series:

  • 152 Accesses

Abstract

We extend process algebra with guards, comparable to the guards in guarded commands or conditions in common programming constructs. The extended language is provided with an operational semantics based on transitions between pairs of a process and a data-state. The data-states are given by a data environment that also defines in which data-states guards hold and how actions (non-deterministically) transform these states. The operational semantics is studied modulo strong bisimulation equivalence. For basic process algebra (without operators for parallelism) we present a small axiom system that is complete with respect to a general class of data environments. In case a data environment S is known, we add three axioms to this system, which is then again complete, provided weakest preconditions are expressible and S is sufficiently deterministic.

Then we study process algebra with parallelism and guards. A two phase-calculus is provided that makes it possible to prove identities between parallel processes. Also this calculus is complete. In the last section we show that partial correctness formulas can easily be expressed in this setting and we use process algebra with guards to prove the soundness of Hoare logic for linear processes by translating proofs in Hoare logic into proofs in process algebra.

(Extended Abstract)

Note: The first author is supported under ESPRIT Basic Research Action no. 3006 (CONCUR) and both authors are supported under RACE project no. 1046 (SPECS) but this document does not necessarily reflect the view of the SPECS consortium.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. D. Austry and G. Boudol. Algèbre de processus et synchronisations. Theoretical Computer Science, 30(1):91–131, 1984.

    Google Scholar 

  2. K.R. Apt. Ten years of Hoare's logic, a survey, part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, 1981.

    Google Scholar 

  3. J.A. Bergstra and J.W. Klop. The algebra of recursively defined processes and the algebra of regular processes. In J. Paredaens, editor, Proceedings 11th ICALP, Antwerp, volume 172 of Lecture Notes in Computer Science, pages 82–95. Springer-Verlag, 1984.

    Google Scholar 

  4. J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

    Google Scholar 

  5. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, Englewood Cliffs, 1976.

    Google Scholar 

  6. J.F. Groote and A. Ponse. Process algebra with guards. Report CS-R9069, CWI, Amsterdam, 1990.

    Google Scholar 

  7. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10), October 1969.

    Google Scholar 

  8. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985.

    Google Scholar 

  9. E.G. Manes and M.A. Arbib. Algebraic Approaches to Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, 1986.

    Google Scholar 

  10. R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

    Google Scholar 

  11. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, pages 319–340, 1976.

    Google Scholar 

  12. G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

    Google Scholar 

  13. A. Ponse. Process expressions and Hoare's logic. Technical Report CS-R8905, CWI, Amsterdam, March 1989. To appear in Information and Computation.

    Google Scholar 

  14. F.M. Sioson. Equational bases of Boolean algebras. Journal of Symbolic Logic, 29(3):115–124, September 1964.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Software Technology, CWI, P.O. Box 4079, 1009 AB, Amsterdam, The Netherlands

    Jan Friso Groote & Alban Ponse

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alban Ponse
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jos C. M. Baeten Jan Frisco Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Groote, J.F., Ponse, A. (1991). Process algebra with guards. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_92

Download citation

  • DOI: https://doi.org/10.1007/3-540-54430-5_92

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54430-2

  • Online ISBN: 978-3-540-38357-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation