Programming Research Group Research Report RR-01-11

Christie Bolton and Jim Davies

June 2001, 96pp.

Abstract

This paper defines a new denotational semantics for the algebraic specification language of Communicating Sequential Processes (CSP). The semantics lies between the existing traces and failures models of CSP, providing a treatment of nondeterminism in terms of singleton failures. Although the semantics does not represent a congruence upon the full language, it is adequate for sequential tests of nondeterministic processes. This semantics corresponds exactly to the relational semantics used for data refinement in Z: an abstract data type is refined in the relational semantics precisely when the corresponding process is refined in the singleton failures semantics. Proofs about data types can therefore be conducted in either semantic domain.