A (possibly-structured) specification may be given a name; subsequent references to the name are equivalent to writing out the specification again.The naming of a specification in CASL serves two main purposes (apart from the purely informal one of suggesting the intentions of the specifier!): to avoid the verbatim repetition of the same specification part within one specification; and to allow its insertion in a library of specifications, so that the specification may be reused simply by referring to its name in all subsequent specifications.
A specification may be made generic, by declaring some parameters which are to be instantiated with `fitting' arguments whenever reference to the name of the specification is made.The parameters of a generic specification are simply dummy parts of the specification (declarations of symbols, axioms) that are intended to be replaced systematically whenever the name of the generic specification is referred to. The classic example is the generic specification of lists of arbitrary items: the parameter specification merely declares the sort of items, which gets replaced by particular sorts (e.g., of integers, characters) when instantiated. For a generic specification of ordered lists, the parameter specification would also declare a binary relation on items, and perhaps insist that it have (at least) the properties of a partial order.
Note that, in contrast to some other specification languages, the parameter here is not a bound variable, whose occurrences in the body (if any) should be replaced by the argument specification. Such a \-calculus form of parametrization would allow the specifier to introduce quite general functions from specifications to specifications; in CASL, the intention is that one always uses the constructs described in this section directly when combining specifications. Moreover, the usefulness of specification functions that ignore their parameter(s) is questionable; with the CASL form of generics, the parameter is automatically extended by the generic specification.
A generic specification may have several parameters. Any common symbols have to be instantiated the same way (the situation is analogous to an extension, where common symbols declared by the specifications that are being extended are regarded as identical). Thus if a generic specification is to have two independent parameters, say pairs of two (possibly) different sorts of items, one has to use different symbols for the two sorts. Although this seems to be a coherent design, CASL does differ in its treatment of parameters from that found in many previous specification languages, so a careful explanation of this point will have to be provided in the supporting manuals and guides.
The semantics of instantiation of generic specifications corresponds to a push-out construction.It is possible to view generic specifications as a particular kind of loose specification, with instantiation having the effect of tightening up the specification. Thus generic lists of items are simply lists where the items have been left (extremely) loosely specified. Instantiating items to integers then amounts to translating the entire specification of lists accordingly (so that e.g. the first argument of the `cons' function is now declared to be an integer rather than an item) and forming its union with the specification of integers--the CASL treatment of common symbols in unions dealing correctly with the two declarations of the sort of integers.
In fact the semantics of instantiation in CASL corresponds closely to the above explanation. Under suitable conditions, it corresponds to a push-out construction on specifications.
The use of compound identifiers for symbols in generic specifications allows the symbols declared by instantiations to depend on the symbols provided by the argument specifications.The observant reader may have noticed that in the example given above, two different instantiations of the generic lists (say, for integers and characters) would declare the same sort symbol for the two different types of lists, causing problems when these get united. CASL allows the use of compound sort identifiers in generic specifications; e.g., the sort of lists may be a symbol formed with the sort of items as a component. The translation of the parameter sort to the argument sort affects this compound sort symbol for lists too, giving distinct symbols for lists of integers and lists of characters, thereby avoiding the danger of unintended identifications and the need for explicit renaming when combining instantiations.