TY - JOUR
T1 - Denotational semantics of communicating sequential programs
AU - Broy, Manfred
PY - 1986/11/24
Y1 - 1986/11/24
N2 - A denotational semantics of Hoare's Communicating Sequential Programs is given based on a mathematical model of communicating processes as functions mapping for every initial state a stream of offers onto a set of streams of reactions plus a final state, which is defined only if the program terminates properly. The main purpose of this definition is found in serving as a reference for specification and verification methods.
AB - A denotational semantics of Hoare's Communicating Sequential Programs is given based on a mathematical model of communicating processes as functions mapping for every initial state a stream of offers onto a set of streams of reactions plus a final state, which is defined only if the program terminates properly. The main purpose of this definition is found in serving as a reference for specification and verification methods.
KW - Communicating processes
KW - denotational semantics
KW - handshake communication
UR - http://www.scopus.com/inward/record.url?scp=0022812207&partnerID=8YFLogxK
U2 - 10.1016/0020-0190(86)90082-7
DO - 10.1016/0020-0190(86)90082-7
M3 - Article
AN - SCOPUS:0022812207
SN - 0020-0190
VL - 23
SP - 253
EP - 259
JO - Information Processing Letters
JF - Information Processing Letters
IS - 5
ER -