Number of rules Static semantics Model Semantics Altogether Basic specifications 109/0 1/0 110/0 Structured specifications 19/29 1/20 20/49 Architectural specifications 0/34 0/34 0/68 Libraries 0/18 0/8 0/26 Altogether 128/81 2/62 130/143 Figure 3: Logic-independence of CASL semantics: The first number counts the logic-dependent rules, the second number the logic-independent rules. The logic-dependent rules of the structured semantics are due to CASL's symbol maps.
Actually, the semantics of CASL-in-the-large (structured and architectural specifications and libraries) is largely independent of the underlying logic. Thus, one can instantiate CASL-in-the-large with different logics (first-order, higher-order, temporal, etc.), and only has to provide a new syntax and semantics of specifications-in-the-small (= basic specifications), while syntax and semantics of specification-in-the-large remains the same (see Fig. 3). This is achieved by working with so-called institutions with symbols [Mos], a notion that allows to mathematically formalize the essential aspects of a logic that are needed for CASL structured specifications.
Indeed, it is actually possible to use this logic-independent semantics to write a logic-independent static analysis of CASL structured specifications. We are currently implementing this as a generic program, which is parameterized over a program doing the analysis for basic specifications, and performing certain operations on signatures that are required by the semantics of CASL structured specifications. Note that it is not practically feasible to parameterize the static analysis directly over an institution with symbols: the semantics of CASL structured specifications involves certain category theoretic constructions which can be carried out in any institution with symbols, but not in a practically feasible way. However, there is only a limited number of such constructions, and the semantics of CASL [CoF99] is written in such a way that these constructions are treated as an abstract datatype (i.e. only they are used when defining the semantics, but not the way they are defined). Thus, the static analysis of CASL structured specifications can be parameterized over a structure containing, apart from static analysis of basic specifications, basically a set of operations implementing these constructions.
What we have described can in principle also be carried over to CASL architectural specifications, though we have not yet begun to work on this, and possible extra complications can be expected (the semantics of CASL architectural specifications is defined over a more complex notion of logic, namely over an arbitrary institution with symbols and sharing).
Finally, CASL libraries are a completely different story - their semantics (and therefore, also their implementation) is entirely orthogonal to the rest of the language and mainly deals with collecting named entities into files that are distributed over the Internet. Here, a general mechanism maintaining officially registered CASL libraries needs to be implemented. We plan to use the UniForM Workbench [KPO+95] for library management, but this is future work.