Denotational Semantics of OCCAM
Yue Qian, Pla Uni · Journal of PLA University of Science and Technology · 2002
A denotational model is presented for a distributed programming language OCCAM/TOY, which is a syntactically simplified version of OCCAM. Communication and classical sequential concepts such as assignment, tests, iteration and guarded commands are featured. The semantics of OCCAM/TOY is presented in the mathematical framework for complete metric spaces. The mathematical model introduces processes as elements of a process domain which is obtained as a solution of a reflexive domain equation over a category of complete metric spaces. A technique has been developed by P.America and J.Bakker to solve a wide class of such equations, including function space constructions. The desired domain is obtained as the fixed point of a contracting function implicit in the equation. Processes are then used as meanings of statements in languages with concurrency, such as OCCAM/TOY.