The crucial point is that structuring a specification does not specify any structure in models! In fact the models of structured specifications are of exactly the same kind as for basic specifications, i.e., algebras interpreting the declared symbols and satisfying all the asserted properties.
For example, consider a specification of the integers. One might choose to structure it as an extension of a specification of natural numbers, rather than giving it as a single basic specification. This choice does not affect the semantics of the specification: neither the signature nor the models reflect the structure of the extension.
Section 5 explains the `architectural' specifications of CASL, which do allow the structure of models to be specified.
A general principle underlying the CASL design is `same name, same thing'. Thus when one sees two occurrences of the same sort in the same basic specification, one may be sure that they are always interpreted as the same carrier set. For operations and predicates, the situation is a little more subtle: the `name' of an operation (or predicate) includes its profile of argument and result sorts, so there need be no relationship at all between say, `+' on integers and `+' on lists or sets, at least in the absence of subsort inclusions.
The `same name, same thing' principle applies also in unions and extensions--but not between named specifications in libraries: the same sort may be used in different named specifications in the same library, with entirely different interpretations; similarly for operations or predicates with the same profiles.
When named specifications are combined in the same structured specification (by references to their names--perhaps indirectly via other named specifications), any unintended clashes can be eliminated by translating the symbols used in them to new ones. From a methodological point of view, it seems indeed appropriate for the writer of a specification to avoid accidental use of the same sort or (qualified) symbol for different purposes, since it could confuse readers. (The same argument does not apply to overloading: for example, use of the ` < ' predicate for partial orders on different sorts is conventional and nicely emphasises their common properties).
Another point is that in CASL, it is easy to hide auxiliary symbols, i.e., symbols that are not inherent to what is to be specified. For example, to specify addition and subtraction on the integers it is common practice to introduce successor and predecessor operations, but they may be regarded as auxiliary and hidden afterwards--they can in any case be recovered using addition and subtraction of 1.
Finally, tools may warn users about multiple declarations of the same name in the same specification, in case they are accidental.
A specification definition names a specification, allowing reuse by reference to the name. For example, Int might refer to a specification of the integers. In CASL, a named specification may also have parameters, intended to vary between references; the specification body is an extension of what is specified in the parameters. Each reference to the specification requires instantiation of all its parameters. For example, List might refer to a specification that extends a parameter specification named Elem; any reference to List has to provide an argument specification that `fits' Elem.
Note that generic extensions in CASL are not intended for defining arbitrary functions on specifications, unlike in some other frameworks such as ASL--the CASL user is expected to express the structure of specifications directly using the CASL language constructs that are provided for that purpose.