Specification-oriented semantics for communicating processes
- 104 Downloads
We are aiming at a classification of semantical models for Communicating Processes that will enable us to recommend certain models which are just detailed enough for particular applications. But before such an aim can be fully realised, more sophisticated models of processes should be studied.
For example, we have not considered the notion of state so far. This would allow to add assignment and explicit value passing between processes, thus combining sequential programs with Communicating Processes.
It is also important to ensure that the operators satisfy the usual algebraic laws, for example parallel composition should be associative. And the relationship between specification-oriented denotational semantics used here and the operational semantics used in [12,13,16] should be studied. This requires an explicit concept of divergence. In particular, it is interesting to investigate how the criterion P sat S can be derived systematically from the operational semantics. A significant step in this direction has already been made in .
Finally, an explicit syntax for specifications and proof systems for the relation P sat S should be developed. First proposals for such proof systems can be found in [5,9].
KeywordsSemantical Model Operational Semantic Proof System Concurrent Program Denotational Semantic
Unable to display preview. Download preview PDF.
- J.W. de Bakker, Mathematical Theory of Program Correctness (Prentice Hall, London, 1980).Google Scholar
- J.W. de Bakker, J.I. Zucker, Denotational semantics of concurrency, in: Proc. 14th ACM Symp. on Theory of Computing (1982) 153–158.Google Scholar
- J.D. Brock, W.B. Ackermann, Scenarios: a model for nondeterminate computations, in: J. Diaz, I. Ramos, Eds., Formalisation of Programming Concepts, LNCS 107 (Springer, Berlin-Heidelberg-New York, 1981) 252–267.Google Scholar
- M. Broy, Fixed point theory for communication and concurrency, in: D. BjØrner, Ed., Formal Description of Programming Concepts II, Preliminary Proc. IFIP TC-2 Working Conference (North Holland, Amsterdam, 1982) 104–126.Google Scholar
- Z. Chaochen, C.A.R. Hoare, Partial correctness of communicating processes, in: Proc. 2nd International Conference on Distributed Computing Systems, Paris (1981).Google Scholar
- N. Francez, C.A.R. Hoare, D.J. Lehmann, W.P. de Roever, Semantics of nondeterminism, concurrency and communication, JCSS 19 (1979) 290–308.Google Scholar
- E.C.R. Hehner, C.A.R. Hoare, A more complete model of communicating processes (to appear in Theoret. Comp. Sci.) 1982.Google Scholar
- C.A.R. Hoare, A model for communicating sequential processes, in: R.M, McKeag, A.M. McNaghton, Eds., On the Construction of Programs (Cambridge University Press, 1980) 229–243.Google Scholar
- C.A.R. Hoare, A calculus of total correctness for communicating processes, Sci. Comp. Programming 1 (1981) 49–72.Google Scholar
- C.A.R. Hoare, Specifications, programs and implementations, Tech. Monograph PRG-29, Oxford Univ., Progr. Research Group, Oxford 1982.Google Scholar
- C.A.R. Hoare, S.D. Brookes, A.W. Roscoe, A theory of communicating sequential processes, Tech. Monograph PRG-16, Oxford Univ., Progr. Research Group, Oxford 1981.Google Scholar
- R. Milner, A calculus of communicating systems, LNCS 92 (Springer, Berlin-Heidelberg-New York, 1980).Google Scholar
- R. Milner, Four combinators for concurrency, in: Proc. ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computations, Ottawa, 1982.Google Scholar
- R. de Nicola, M.C.B. Hennessy, Testing equivalences for processes, Internal Report CSR-123-82, Univ. of Edinburgh, Computer Science Dept., 1982.Google Scholar
- S. Owicki, L. Lamport, Proving liveness properties of concurrent programs, ACM TOPLAS 4 (1982) 455–495.Google Scholar
- G.D. Plotkin, An operational semantics for CSP, in: D. BjØrner, Ed., Formal Description of Programming Concepts II, Preliminary Proc IFIP TC-2 Working Conference (North Holland, Amsterdam, 1982) 185–208.Google Scholar
- D.S. Scott, Domains for denotational semantics, in: M. Nielsen, E.M. Schmidt, Eds., Proc. 9th ICALP, LNCS 140 (Springer, Berin-Heidel berg-New York, 1982) 577–613.Google Scholar
- M.B. Smyth, Power domains, JCSS 16 (1978) 23–26.Google Scholar