Both Lawrence's HCSP [1] and Smith, et al's VCR, [2] (an earlier version appears in [3]) extend CSP [4] with representations of truly concurrent events. Previously, VCR, was described using an operational semantics, while the semantics of HCSP's Acceptances model, like those of the predominant CSP models described by Roscoe [5] (e.g., Traces, Failures / Divergences), are denotational. We now present a denotational semantics for VCR. and, in so doing, propose an extension to HCSP (and possibly other existing CSP models) to support View-Centric Reasoning. This work brings VCR. a step closer to being drawn within Hoare and He's Unifying Theories of Programming [6] for further comparisons.
展开▼
