zbMATH — the first resource for mathematics

The laws of Occam programming. (English) Zbl 0719.68039
The authors describe an equational axiomatization of the semantics of OCCAM. They show that WHILE-free programs have a normal form, such that two programs are semantically equivalent if and only if their normal forms are syntactically equivalent. This shows that their equational axiomatization, together with an induction axiom, is a sound and complete proof system for proving the equivalence of OCCAM programs. The paper is very clearly written.

68Q55 Semantics in the theory of computing
68N15 Theory of programming languages
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI
[1] Apt, K.R.; Francez, N.; De Roever, W.P., A proof system for communicating sequential processes, ACM trans. programming language systems, 2, 3, 359-385, (1980) · Zbl 0468.68023
[2] Brookes, S.D., A model for communicating sequential processes, (), (available as a Carnegie-Mellon University technical report) · Zbl 0565.68023
[3] Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[4] Fisher, A., Formal number theory and computability, () · Zbl 0504.03002
[5] Guessarian, I., Algebraic semantics, () · Zbl 0602.68017
[6] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[7] The Occam programming manual, (1984), Prentice-Hall Englewood Cliffs, NJ
[8] Hoare, C.A.R.; He, Jifeng; Hayes, I.J.; Morgan, C.C.; Sanders, J.W.; Sørensen, I.H.; Spivey, J.M.; Sufrin, B.A.; Roscoe, A.W., Laws of programming, Comm. ACM, 30, 8, 672-686, (1987) · Zbl 0629.68006
[9] Roscoe, A.W., Denotational semantics for Occam, (), 306-329, Version (b) to appear as a PRG monograph, Oxford University Computing Laboratory. · Zbl 0565.68024
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.