Denotational semantics of communicating sequential programs (Q1088402)

The language CSP (Communicating Sequential Programs) of Hoare is an elegant notation for the description of communicating systems. A denotational semantics of CSP is given based on a mathematical functional model of communicating processes by functions mapping for every initial state an input stream, i.e. a finite or infinite sequence, of offers onto a set of output streams of reactions plus a final state which is defined only if the program terminates properly. An offer is either the request for sending the value of a variable or the offer to send the value of a variable. A reaction is either the value of a variable requested or the acknowledgement for a value offered or a reject signal. The reject signal is only given as output if an offer cannot be accepted. This gives a very general view of communicating processes as stimulus/response systems. The main purpose of this definition is found in serving as a reference for specification and verification methods.