zbMATH — the first resource for mathematics

A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. (English) Zbl 0992.68026
Summary: This paper introduces a compositional Hoare logic for reasoning about the partial correctness and absence of deadlock of a certain class of programs. Considered are programs that describe networks composed of a dynamically evolving collection of processes which are all executing in parallel, and which know each other by maintaining and passing around process-references via an asynchronous communication mechanism based on (unbounded) FIFO buffers. The Hoare logic formalizes reasoning about such dynamic networks on an abstraction level that is at least as high as that of the programming language. This means that the only operations on ‘pointers’ (that is, references to processes) are testing for equality and dereferencing. Moreover, in a given state of the system, it is only possible to mention the processes that exist in that state. Processes that have not (yet) been created do not play a role. Soundness and completeness of the logic is proved with respect to a compositional characterization of the initial/final state semantics of programs. This characterization generalizes the compositional semantics of deterministic Kahn (data-flow) networks (where the number of processes and communication structure is fixed).

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Full Text: DOI
[1] M. Abadi, K.R.M. Leino, A logic of object-oriented programs, Proc. 7th Internat. J. Conf. CAAP/FASE, Lecture Notes in Computer Science, vol. 1214, April 1997. · Zbl 1274.68055
[2] P. America, F.S. de Boer, Reasoning about dynamically evolving process structures, Formal Aspects Comput. 6(3) (1994). · Zbl 0821.68106
[3] Apt, K.R., Ten years of Hoare logic: a survey – part I, ACM, trans. programming languages systems, 3, 4, 431-483, (1981) · Zbl 0471.68006
[4] F. Arbab, E.P.B.M. Rutten, Manifold: a programming model for massive parallelism, Proc. IEEE Working Conf. on Massively Parallel Programming Models, Berlin, 1993.
[5] de Bakker, J.W., Mathematical theory of program correctness, (1980), Prentice-Hall Englewood Cliffs, NJ
[6] F.S. de Boer, Reasoning about dynamically evolving process structures (a proof theory of the parallel object-oriented language POOL), Ph.D. Thesis, Free University, Amsterdam, 1991.
[7] de Boer, F.S., A compositional proof system for dynamic process creation, proc. 6th annual IEEE symp. on logics in computer science (LICS), (1991), IEEE Computer Society Press Amsterdam, The Netherlands
[8] Goldberg, A.; Robson, D., Smalltalk-80, the language and its implementation, (1983), Addison-Wesley Reading, MA · Zbl 0518.68001
[9] Kahn, G., The semantics of a simple language for parallel programming, IFIP74 congress, (1974), North-Holland Amsterdam
[10] A. Poetzsch, P. Mueller, Logical foundations for typed object-oriented languages, Proc. IFIP Working Conf. on Programming Concepts and Methods, PROCOMET98.
[11] Scott, D.S., Identity and existence in intuitionistic logic, (), 660-696
[12] Tucker, J.V.; Zucker, J.I., Program correctness over abstract data types, with error-state semantics, CWI monograph series, vol. 6, centre for mathematics and computer science, (1988), North-Holland Amsterdam · Zbl 0641.68028
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.