×

zbMATH — the first resource for mathematics

Reasoning about dynamically evolving process structures. (English) Zbl 0821.68106
Summary: We develop a Hoare-style proof system for reasoning about the behaviour of processes that interact via a dynamically evolving communication structure.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T27 Logic in artificial intelligence
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Software:
Eiffel; Smalltalk
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] America, P. H. M: Issues in the Design of a Parallel Object-Oriented Language.Formal Aspects of Computing,1, 366-411 (1989). · Zbl 0694.68012 · doi:10.1007/BF01887214
[2] 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. · Zbl 0695.68058
[3] 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). · Zbl 0468.68023 · doi:10.1145/357103.357110
[4] Apt, K. R.: Ten Years of Hoare logic: A Survey?Part I.ACM Transactions on Programming Languages and Systems,3, 431-483 (1981). · Zbl 0471.68006 · doi:10.1145/357146.357150
[5] Apt, K. R.: Formal Justification of a Proof System for Communicating Sequential Processes.Journal of the ACM,30, 197-216 (1983). · Zbl 0503.68021 · doi:10.1145/322358.322372
[6] de Bakker, J. W.:Mathematical Theory of Program Correctness. Prentice-Hall International, 1980. · Zbl 0452.68011
[7] Goldberg, A. and Robson, D.:Smalltalk-80, The Language and its Implementation. Addison-Wesley, 1984. · Zbl 0518.68001
[8] Hoare, C. A. R.: An Axiomatic Basis for Computer Programming.Communications of the ACM,12, 567-580,583 (1969). · Zbl 0179.23105 · doi:10.1145/363235.363259
[9] Hoare, C. A. R.: Communicating Sequential Processes.Communications of the ACM,21, 666-677 (1978). · Zbl 0383.68028 · doi:10.1145/359576.359585
[10] 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.
[11] 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). · Zbl 0731.68076
[12] Meyer, B.:Object-Oriented Software Construction. Prentice-Hall, 1988. · Zbl 0719.68012
[13] Tucker, J. V. and Zucker, J. I.:Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monographs 6, North-Holland, 1988. · Zbl 0641.68028
[14] 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. · Zbl 0566.68014
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.