Beschreibung:
In this paper, we address the problem of specification and design of concurrent systems More accurately, we present the definition of a new specification language that is formal, wide-spectrum, model-based, concurrent, polymorphic, and strongly implicitly typed The lan guage is built upon a concurrent, functional, and imperative programming language Concurrent ML Specification aspects are supported thanks to the addition of some specification constructs and also by allowing axioms to appear in ML structures and signatures The resulting specification language is thus highly expressive though it embodies a restricted number of concepts We present here the motivations underlying the definition of such a language as well as the design choices Furthermore, we introduce the specification and development methodology and illustrate it on various examples We will see that many specification styles are allowed algebraic, applicative, state-based, concurrent applicative, and con current imperative