A Methodology for Concurrent Languages Development Based on Denotational Semantics

摘要

By using the "continuation semantics for concurrency" (CSC) technique [6] denotational semantics can be used both as a method for formal specification and as a general method for designing tractable compositional prototypes for concurrent languages [8]. A denotational specification produces as final yield an element of a classic power domain structure. A denotational prototype designed with CSC produces incrementally a single execution trace and uses a random number generator to model the nondeterminism of a "real" concurrent system. In this paper we present a methodology for concurrent languages development based on denotational semantics. The main step of this methodology is the establishment of the formal relationship between a denotational prototype and a corresponding denotational specification. We illustrate this methodology on the particular example of a CSP-like language extended with communication on multiple channels in the style of Join calculus. We employ techniques from metric semantics in designing and relating the denotational prototype and the denotational specification for the language under study. We prove that the (single) trace produced by the denotational prototype is always an element of the collection of traces that is produced by the denotational specification. This result is independent of the random number generator that is given as a parameter to the denotational prototype.