Whereas the structuring of specifications into unions and extensions encourages the reuse of (self-contained) parts of specifications, it does not affect the models at all, and the monolithic result of implementing a structured specification is unlikely to be reusable. To allow implementation units to be reusable, CASL provides further constructs for the specification of structure.
For a simple example, suppose that one wishes to structure the implementation of List [Nat] to include:
These are the explicit assumptions that parts of an implementation make about other parts. In CASL, interfaces are expressed as ordinary (structured) specifications, asserting that the symbols declared by the specification not only have to be implemented, but also have to satisfy all the asserted properties. A specification of a functional unit involves the specifications of all its arguments and of its result. It is guaranteed that the results of applying functional units to argument units will meet their target specifications, provided that the argument units meet their given specifications.
A crucial aspect of architectural specifications is that they provide decompositions of (possibly large) implementation development tasks into smaller sub-tasks--as well as indicating how to compose (or link together) the results of sub-tasks. A unit specification expresses all that those who are implementing it need to know.
It is clearly desirable to distinguish between structure of specifications and specification of structure, so that specifying (e.g.) Int as an extension of Nat does not require separate implementations of these two specifications. What may not be quite so obvious is that the distinction is actually essential--at least if one is using the familiar specification structuring constructs provided by CASL. Consider the union of two specifications with some declared common symbols but different axioms: if each specification is implemented separately, without taking account of the properties required by the other specification, it may well happen that the common symbols have different, incompatible implementations which cannot be combined.