Abstract
We develop a Hoare-style proof system for reasoning about the behaviour of processes that interact via a dynamically evolving communication structure.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
America, P. H. M: Issues in the Design of a Parallel Object-Oriented Language.Formal Aspects of Computing,1, 366–411 (1989).
America, P. H. M., de Bakker, J. W., Kok, J. N. and Rutten, J. J. M. M.: Operational Semantics of a Parallel Object-Oriented Language.Conference Record of the 13th Symposium on Principles of Programming Languages, St. Petersburg, Florida, pp. 194–208, 1986.
Apt, K. R., Francez, N. and de Roever, W. P.: A Proof System for Communicating Sequential Processes.ACM Transactions on Programming Languages and Systems,2, 359–385 (1980).
Apt, K. R.: Ten Years of Hoare logic: A Survey—Part I.ACM Transactions on Programming Languages and Systems,3, 431–483 (1981).
Apt, K. R.: Formal Justification of a Proof System for Communicating Sequential Processes.Journal of the ACM,30, 197–216 (1983).
de Bakker, J. W.:Mathematical Theory of Program Correctness. Prentice-Hall International, 1980.
Goldberg, A. and Robson, D.:Smalltalk-80, The Language and its Implementation. Addison-Wesley, 1984.
Hoare, C. A. R.: An Axiomatic Basis for Computer Programming.Communications of the ACM,12, 567–580,583 (1969).
Hoare, C. A. R.: Communicating Sequential Processes.Communications of the ACM,21, 666–677 (1978).
Hooman, J. and de Roever, W. P.: The Quest Goes On: Towards Compositional Proof Systems for CSP. In J.W. de Bakker, W.P. de Roever, G. Rozenberg (eds.):Current Trends in Concurrency, Springer LNCS 224, pp. 343–395, 1986.
Meldal, S.: Axiomatic Semantics of Access Type Tasks in Ada. Report No. 100, Institute of Informatics, University of Oslo, Norway, May 1986. Appeared as “Complete Axiomatic Semantics of Spawning,”Distributed Computing,3, 159–174 (1991).
Meyer, B.:Object-Oriented Software Construction. Prentice-Hall, 1988.
Tucker, J. V. and Zucker, J. I.:Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monographs 6, North-Holland, 1988.
Zwiers, J., de Roever, W. P. and van Emde Boas, P.: Compositionality and concurrent networks: soundness and completeness of a proof system.Proceedings of the 12th ICALP, Nafplion, Greece, Springer LNCS 194, pp. 509–519, 1985.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
America, P., de Boer, F. Reasoning about dynamically evolving process structures. Formal Aspects of Computing 6, 269–316 (1994). https://doi.org/10.1007/BF01215408
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01215408