This section provides examples that illustrate the CASL language constructs for use in structured specifications: translation, reduction, union, extension, free extension, local specifications, specification definitions, generic parameters, instantiation, views, and compound identifiers.
Translation of declared symbols to new symbols is specified straightforwardly by giving a list of `maplets' of the form old |-> new. Identity maplets old |-> old may be abbreviated to old, or simply omitted altogether. Optionally, the nature of the symbols concerned (sorts, operations, predicates) may be indicated by inserting the corresponding keywords.
- Nat with Nat |-> Natural, suc |-> succ__
- Nat with op __+__ |-> plus, pred __<__ |-> lt
Reduction means removing symbols from the signature of a specification, and removing the corresponding items from models. When a sort is removed, so are all operations and predicates whose profiles include that sort. CASL provides two ways of specifying a reduction: by listing the symbols to be hidden, or by listing those to be left visible, i.e., revealed. In the latter case, (some of) the revealed symbols may also be translated to new symbols.
- Nat hide Pos, suc
- Nat reveal Nat, 0, __+__ , __<__ |-> lt
The signature of a union of two (or more) specifications is the union of their signatures. The models of a union are those whose reducts to the component signatures are models of the component specifications. There are two extremes: when the specifications have disjoint signatures, their union provides amalgamation of their models; when they have the same signature, it provides the intersection of the model classes, giving models that satisfy both the specifications at once. For example, the signatures of Nat and String might be disjoint, so models of
would be amalgamations of models of Nat and of String, whereas the signatures of Monoid and Commutative might be the same, so models of
- Nat and String
would be those that are simultaneously models of Monoid and of Commutative (i.e., commutative monoids).
- Monoid and Commutative
Extensions may specify new symbols (known as enrichment):
or merely require further properties of old ones:
- Nat then
- sort
- Nat < Int ;
- ops
- __+__ : Int × Int -> Int;
...
An extension is called conservative when no models are lost: every model of the specification being extended is a reduct of some model of the extended specification. Whether an extension is conservative or not may be indicated by an annotation (not illustrated here).5
- Collection then
- axiom
- forall c:Collection · join(c,c) = c
The simplest case of a free specification is when the component specification is self-contained. The signature of the specification is unchanged, but the models are restricted to (the isomorphism class of) its initial models. E.g., the only models of the following specification are the standard models of Peano's axioms:
The conciseness and perspicuity of such specifications may account for the popularity of frameworks that support initiality. When axioms are restricted to positive conditional existential equations, initial models always exist.
- free
- {
- sort Nat; ops 0 : Nat ; suc : Nat -> Nat }
More generally, a free specification may be a free extension, e.g.:
Note that free specifications are especially useful for inductively-defined predicates, since only the cases where the predicates hold need be given: all other cases are automatically false. Similarly for partial operations in a free specification, which are as undefined as possible in all its models.
- sort
- Elem then
- free
- {
- type
- Set ::= Ø | {|__|}(Elem) | __ u __(Set; Set)
- op
- __ u __ : Set × Set -> Set, assoc, comm, idem, unit Ø }
CASL facilitates the hiding of auxiliary symbols by allowing the local scope of their declarations to be indicated. E.g., suc below is an auxiliary symbol for use in specifying addition:
Ideally, the operations and predicates of interest are specified directly by their properties, without the introduction of auxiliary symbols that have to be hidden. However, there are classes of models that cannot be specified (finitely) without the use of auxiliary symbols; in other cases the introduction of auxiliary symbols may lead `merely' to increased conciseness and perspicuity.
- sort
- Nat
- op
- 0 : Nat
- then local
- op
- suc : Nat -> Nat
- within
- op
- __+__ : Nat × Nat -> Nat
- vars
- m, n : Nat
- ·
- m+0 = m
- ·
- m+suc(n) = suc(m+n)
Only self-contained specifications can be named--the local environment for a named specification is always empty. Named specifications are intended for inclusion in libraries, see Section 6. Subsequent specifications in the library (or in other libraries) may include a copy of the named specification simply by referring to its name, e.g.:
- spec
- Nat = free { ... }
- spec
- Int = Nat then free { ... }
A parameter is a closed subspecification--typically a reference to a rather simple named specification such as Elem:
A named specification is essentially an extension of all its parameters. A reference to a named specification with parameters is called an instantiation, and has to provide an argument specification for each parameter, indicating how it `fits' by giving a map from the parameter signature to the argument signature, e.g.:
- spec
- Elem = sort Elem
- spec
- List [Elem] =
free type List ::= nil | cons(Elem; List)
List [Nat fit Elem |-> Nat]Since there is only one possible signature morphism from Elem to Nat, the fitting may be left implicit, and the instantiation written may be written simply as List [Nat]. As with translation maps, identity fittings may always be omitted. Of course the map is required to induce not just a signature morphism but also a specification morphism: all models of the argument specification must also be models of the parameter specification.
Sharing between parameter symbols is preserved by fitting, so it may be necessary to rename symbols when separate instantiation of similar parameters is required, e.g.:
Note that the `same name, same thing' principle is maintained here. Moreover, to use the same sort name (say Elem) in both parameters would require some way of disambiguating the different uses of the name in the body, similar to an explicit renaming.
- spec
- Pair [sort Elem1] [sort Elem2] =
free type Pair ::= pair(Elem1; Elem2)
Sharing of symbols between the body of a generic specification and its arguments in an instantiation is restricted to explicit imports, indicated as `given':
Well-formed instantiations always have a `push-out' semantics. Had Nat been merely referenced in the body of List_Length, an instantiation such as
- spec
- List_Length [Elem] given Nat =
- free type
- List ::= nil | cons(Elem; List)
- op
- length : List -> Nat
Suppose that two different instantiations of List are combined, e.g.,
List [Nat fit Elem |-> Nat] and List [Char fit Elem |-> Char]With the previous definition of List, an unintentional name clash arises: the sort List is declared by both instantiations, but clearly should have different interpretations. To avoid the need for explicit renaming in such circumstances, compound identifiers such as List[Elem] may be used:
Now when this List is instantiated, the translation induced by the fitting morphism is applied to the component Elem also where it occurs in List[Elem], so the sorts in the above instantiations are now distinct: List[Nat] and List[Char].
- spec
- List [Elem] =
free type List[Elem] ::= nil | cons(Elem; List[Elem])
To allow reuse of fitting `views', specification morphisms (from parameters to arguments) may be themselves named, e.g.:
The syntax for referencing a named specification morphism, e.g.:
- spec
- PO2Nat : Partial_Order to Nat =
Elem |-> Nat, __ < __ |-> __ < __
List_with_Order [view PO2Nat]makes it clear that the argument is not merely some named specification with an implicit fitting map, which would be written simply List_with_Order [Nat]
The rules regarding omission of `evident' maps in explicit fittings apply to named specification morphisms too.