3 Requirement versus Design Specifications

3 Requirement versus Design Specifications

The guidelines presented in this section depend on the type of a specification. We distinguish between requirement and design specifications in the following sense: requirement specifications are loose, i.e. the specifier conciously leaves certain properties unspecified. Thus, the specified datatypes are polymorphic and, as a consequence, the specification is `incomplete': given a property in terms of a formula, neither this formula nor its negation might hold for the whole model class. In contrast to this, design specifications are complete: all design decision have been taken and the specified model class is monomorphic.

For parametrized specifications, this pictures becomes more involved. In general, CASL specification definitions are of the form

spec

SN [SP₁] ...[SP_n] given SP"₁, ..., SP"_m =

SP

end

The annotation %mono shall express that the extension of

With these definitions, we obtain as guidelines concerning instantiations:

1. Instantiating the parameters of a requirement specification yields a requirement specification.
2. Instantiating the parameters of a design specification with design specifications yields a design specification.
3. Instantiating the parameters of a design specification with requirement specifications, which stem from a foramal parameter, yields a design specification. Otherwise, one obtains a requirement specification.

3 Requirement versus Design Specifications