Specifications of independent items may be combined, and subsequently extended with specification of further sorts, subsort embeddings, functions, predicates, and/or properties.The most fundamental way of combining two independent specifications is to take their union. Models of the united specification have to provide interpretations of all the symbols from the two specifications. The provision of union allows independent parts of a specification to be presented separately, thereby increasing the likelihood that they will be reusable in various contexts. CASL provides a construct for taking the union of any number of specifications, generalizing the binary union (which is associative).
Extension of a specification allows the addition of further functions (and predicates) on already-specified sorts, perhaps adding new sorts as well. It is also possible with extension to add further properties, either concerning already-specified symbols or ones being introduced in the extension itself. The CASL construct for extension allows arbitrary further bits of structured specification to be added in a particular order.
It may be declared whether or not the models of the specifications being extended are to be preserved.The case where an extension is `conservative', not disturbing the models of the specifications being extended, occurs frequently. For example, when specifying a new function on numbers, one does not intend to change the models for numbers. For convenience, CASL allows the specifier to indicate that a whole series of extensions are all conservative. Note that while ordinary binary and conservative extension are separately associative, mixtures of them may be affected by the grouping.
The identical declaration of the same symbol in specifications that get combined is regarded as intentional.Suppose that one unites two specifications that both declare the same symbol: the same sort, or functions or predicates with the same profiles. If this is regarded as well-formed (as it is in CASL) there are potentially (at least) two different interpretations: either the common symbol is regarded as shared, giving rise to a single symbol in the signature of the union, satisfying both the given specifications; or the two symbols are regarded as homonyms, i.e., different entities with the same name, which have somehow to be distinguished in the signature of the union.
CASL, following ASL and LARCH, takes the former interpretation, since the symbols declared by a specification (and not hidden) are assumed to denote entities of interest to the user, and unambiguous notation should be used for them. This treatment also has the advantage of semantic simplicity. However, due to the possibility of unintentional `clashes' between accidentally-left-unhidden auxiliary symbols, it is envisaged that CASL tools will be able to warn users about such cases. Note that when the two declarations of the symbol arise from the same original specification via separate extensions that later get united, the CASL interpretation gives the intended semantics, and moreover in such cases no warnings need be generated by tools.
CASL provides a construct for local specification, which combines the effects of extension and hiding. By use of this construct, one may distinguish clearly between declarations of auxiliary symbols and those of required symbols. Moreover, one does not have to specify a separate list of the symbols that are to be hidden.