The structure of a specification does not require models to have any corresponding structure.The structuring constructs considered in the preceding section allow a large specification to be presented in small, logically-organized parts, with the pragmatic benefits of comprehensibility and reusability. In CASL, the use of these constructs has absolutely no consequences for the structure of models, i.e., of the code that implements the specification. For instance, one may specify integers as an extension of natural numbers, or specify both together in a single basic specification; the models are the same.
It is especially important to bear this in mind in connection with generic specifications. The definition of a generic specification of lists of arbitrary items, and its instantiation on integers, does not imply that the implementation has to provide a parametrized program module for generic lists: all that is required is to provide lists of integers (although the implementor is free to choose to use a parametrized module, of course). Sannella, Sokolowski, and Tarlecki [SST92] provide extensive further discussion of these issues.
In contrast, an architectural specification requires that any model should consist of a collection of separate component units that can be composed in a particular way to give a resulting unit. Each component unit is to be implemented separately, providing a decomposition of the implementation task into separate subtasks with clear interfaces.In CASL, an architectural specification consists of a collection of component unit specifications, together with a description of how the implemented units are to be composed. A model of such a specification consists of a model for each component unit specification, and the described composition.
A unit may be required to provide an extension of other units that are being implemented separately. The compatibility of implementations of any common declared symbols in the extended units has to be ensured.In general, the individual units may be regarded as functions: they correspond to parametrized program modules that extend their arguments. For example, one may specify a unit that is to extend any implementation of integers with an implementation of lists of integers, thus separating the task of implementing integers as a self-contained sub-task, and with the implementation of lists being allowed to apply the specified functions and predicates on integers. The specification of a unit consists of the specification of each argument that is to be extended, and the specification of the extension itself. These argument and result specifications form the interfaces of the unit.
A unit implementing lists of integers is not allowed to replace the implementation of integers by a different one! The argument has to be preserved, i.e., the unit has to be a persistent function. To cater for this, the result signature of each unit has to include each argument signature--any desired hiding has to be left to when units are composed. Since each symbol in the union of the argument signatures has to be implemented the same way in the result as in each argument where it occurs, the arguments must already have the same implementation of all common symbols. In CASL, this is built into the semantics of architectural specifications, and the specifier does not have to spell out the intended identity between parts of arguments, nor between arguments and results (in contrast to a previous approach to architectural specifications [SST92]). The description of the composition of units is only well-formed when it ensures that units with potentially-incompatible implementations of the same symbols cannot be combined as arguments.
When the resulting unit is composed, the symbols defined by a unit may be translated or hidden.In the example considered above, one may alternatively specify a more general unit that it is to extend any implementation of arbitrary items (not just implementations of integers) with lists. Such a unit can then be applied to an implementation of integers, the required fitting of items to integers being described as part of the composition of units.
Architectural specifications and the specifications of their components may be named, and subsequently referenced.Although architectural and component specifications have different semantics and usage compared to structured specifications, there is a similar need to be able to name them and reuse them by simply referring to their names.