Specification-oriented semantics for Communicating Processes

Ernst-Rüdiger Olderog1, C. A. R. Hoare2
1Institut für Informatik und Praktische Mathematik Christian-Albrechts-Universität Kiel, Kiel 1, Germany
2Programming Research Group, Oxford University Computing Laboratory, Oxford, UK

Tóm tắt

Từ khóa


Tài liệu tham khảo

Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM TOPLAS 2, 359–385 (1980)

Apt, K.R.: Formal justification of a proof system for communicating sequential processes. J. Assoc. Comput. Mach. 30, 197–216 (1983)

de Bakker, J.W.: Mathematical theory of program correctness. London: Prentice Hall 1980

de Bakker, J.W., Bergstra, J.A., Klop, J.W., Meyer, J.-J.C.: Linear time and branching time semantics for recursion with merge. TCS 34, 134–156 (1984)

de Bakker, J.W., Meyer, J.-J.C., Olderog, E.-R.: Infinite streams and finite observations in the semantics of uniform concurrency. In: Proc. 12th Coll. Automata, Languages and Programming. (W. Brauer ed.). Lect. Notes Comput. Sci. 194, 149–157 (1985)

de Bakker, J.W., Meyer, J.-J.C., Olderog, E.-R., Zucker, J.I.: Transition systems, infinitary languages and the semantics of uniform concurrency. In: Proc. 17th ACM Symposium on Theory of Computing, pp. 252–262. Providence 1985

de Bakker, J.W., Zucker, J.I.: Processes and the denotational semantics of concurrency. Inf. Control 54, 70–120 (1982)

Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. TCS 37, 77–121 (1985)

Bergstra, J.A., Klop, J.W., Olderog, E.-R.: Readies and failures in the algebra of communicating processes. Report CS-R8523, Center for Mathematics and Computer Science, Amsterdam 1985

Brock, J.D., Ackermann, W.B.: Scenarios: a model for nondeterminate computations. In: Formalisation of Programming Concepts (J. Diaz, I. Ramos, eds.). Lect. Notes Comput. Sci. 107, 252–267 (1981)

Brookes, S.D.: A model for communicating sequential processes. D. Phil. Thesis, Oxford Univ. 1983

Brookes, S.D.: On the relationship of CCS and CSP. In: Proc. 10th Coll. Automata, Languages and Programming (J. Diaz, ed.). Lect. Notes Comput. Sci. 154, 83–96 (1983)

Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. Assoc. Comput. Mach. 31, 560–599 (1984)

Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating sequential processes. In: Proc. NSF-SERC Seminar on Concurrency. Lect. Notes Comput. Sci. 197, 281–305 (1985)

Broy, M.: Fixed point theory for communication and concurrency. In: Formal Description of Programming Concepts II (D. Bjørner, ed.), pp. 125–146. Amsterdam: North Holland 1983

Chaochen, Z., Hoare, C.A.R.: Partial correctness of communicating processes. In: Proc. 2nd International Conference on Distributed Computing Systems. Paris 1981

Francez, N., Hoare, C.A.R., Lehmann, D.J., de Roever, W.P.: Semantics of nondeterminism, concurrency and communication. J. Comput. Syst. Sci. 19, 290–308 (1979)

Francez, N., Lehmann, D., Pnueli, A.: A linear history semantics for languages for distributed programming. TCS 32, 25–46 (1984)

Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. J. Assoc. Comput. Mach. 24, 68–95 (1977)

Guessarian, I.: Algebraic semantics. Lect. Notes Comput. Sci. 99 (1981)

Hehner, E.C.R.: Predicative programming, Part I and II. Commun. ACM 27, 134–151 (1984)

Hehner, E.C.R., Hoare, C.A.R.: A more complete model of communicating processes. TCS 26, 105–120 (1983)

Hennessy, M.: Acceptance trees. J. Assoc. Comput. Mach. 32, 896–928 (1985)

Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32, 137–161 (1985)

Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21, 666–677 (1978)

Hoare, C.A.R.: A model for communicating sequential processes. In: On the Construction of Programs (R.M. McKeag, A.M. McNaghton, eds.), pp. 229–243. Cambridge: University Press 1980

Hoare, C.A.R.: A calculus of total correctness for communicating processes. Sci. Comput. Program. 1, 49–72 (1981)

Hoare, C.A.R.: Specifications, programs and implementations. Tech. Monograph PRG-29, Progr. Research Group. Oxford University 1982

Hoare, C.A.R.: Communicating sequential processes. London: Prentice Hall 1985

INMOS: OCCAM programming manual. London: Prentice Hall 1984

Jorrand, P.: Specification of communicating processes and process implementation correctness. In: Proc. 5th Intern. Symp. on Programming. (M. Dezani-Ciancaglini, U. Montanari, eds.). Lect. Notes Comput. Sci. 137, 242–256 (1983)

Keller, R.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)

Levin, G.M., Gries, D.: A proof technique for communicating sequential processes. Acta Inf. 15, 281–302 (1981)

Milner, R.: A calculus of communicating systems. Lect. Notes Comput. Sci. 92 (1980)

Milner, R.: A modal characterisation of observable machine-behaviour. In: Proc. 6th Coll. Trees in Algebra and Programming (E. Asteriano, C. Böhm, eds.). Lect. Notes Comput. Sci. 112, 25–34 (1981)

Milner, R.: Calculi for synchrony and asynchrony. TCS 25, 267–310 (1983)

Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7, 417–426 (1981)

Misra, J., Chandy, K.M., Smith, T.: Proving safety and liveness of communicating processes with examples. In: Proc. 1st ACM SIGACT-SIGOPS Symp. Principles of Distributed Computing, pp. 201–208. Ottawa 1982

de Nicola, R.: A complete set of axioms for a theory of communicating sequential processes. In: Proc. Intern. Conf. on Foundations of Computation Theory (M. Karpinski, ed.). Lect. Notes Comput. Sci. 158, 115–126 (1983)

de Nicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83–134 (1984)

Olderog, E.-R.: Specification-oriented programming in TCSP. In: Logics and Models of Concurrent Systems (K.R. Apt, ed.), pp. 397–435. Berlin, Heidelberg, New York: Springer 1985

Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes (preliminary version). In: Proc. 10th Coll. Automata, Languages and Programming (J. Diaz, ed.). Lect. Notes Comput. Sci. 154, 561–572 (1983)

Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM TOPLAS 4, 455–495 (1982)

Plotkin, G.D.: An operational semantics for CSP. In: Formal Description of Programming Concepts II (D. Bjørner, ed.), pp. 199–223. Amsterdam: North Holland 1983

Reinecke, R.: Networks of communicating processes: a functional implementation. Manuscript, Dept. Comput. Sci., Univ. of Kaiserslautern 1983

Roscoe, A.W.: A mathematical theory of communicating processes. D. Phil., Thesis, Oxford Univ. 1982

Rounds, W.C., Brookes, S.D.: Possible futures, acceptances, refusals and communicating processes. In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, Nashville, Tennessee 1981

Smyth, M.B.: Power domains. J. Comput. Syst. Sci. 16, 23–26 (1978)

Soundararajan, N., Dahl, O.-J.: Partial correctness semantics of communicating sequential processes. Research Rep. No. 66, Inst. of Informatics, Univ. of Oslo 1982

Stoy, J.E.: Denotational semantics: the Scott-Strachey approach to programming language theory. Cambridge: MIT Press 1977

Winskel, G.: Events in computation. Ph. D. Thesis, Dept. Comput. Sci., Univ. of Edinburgh 1980

Zwiers, J., de Roever, W.P., van Emde Boas, P.: Compositionality and concurrent networks. In: Proc. 12th Coll. Automata, Languages and Programming (W. Brauer, ed.). Lect. Notes Comput. Sci. 194, 509–519 (1985)