Go backward to Translation and Hiding
Go up to CASL
Go forward to Initiality and Freeness

Union and Extension

Specifications of independent items may be combined, and subsequently extended with specification of further sorts, 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.

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 to the union of any number of specifications. In fact union itself is essentially just an empty extension.

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 generality, CASL allows the specifier to indicate for each of the extended specifications whether its models are intended to be preserved or not.
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.


CoFI Tentative Document: Mosses97TAPSOFT --TAPSOFT'97-- April 1997.
Comments to pdmosses@brics.dk