CASL is a specification language that can be used for formal development and verification of software. It covers both the level of requirement specifications, which are close to informal requirements, and of design specifications, which are close to implemented programs. CASL provides constructs for writing
Basic CASL specifications consist of declarations and axioms representing theories of a first-order logic in which predicates, total as well as partial functions, and subsorts are allowed. Predicate and function symbols may be overloaded [CHKBM97]. Datatype declarations allow to shortly describe the usual datatypes occurring in programming languages.
Structured specifications allow to rename or hide parts of specifications, unite, extend and name specifications. Moreover, generic specifications and views allow to abstract from particular parts of a specification, which makes the specification reusable in different context.
Architectural specifications allow to talk about implementation units and their composition to an implementation of a larger specification (or, vice versa, the decomposition of an implementation task into smaller sub-tasks).
Structured and architectural specifications together with libraries will be also referred to as CASL-in-the-large, while basic specifications will be referred to as CASL-in-the-small.
Number of rules Static semantics Model Semantics Altogether Basic specifications 109 1 110 Structured specifications 48 21 69 Architectural specifications 34 34 68 Libraries 18 8 26 Altogether 209 64 273 Figure 1: Complexity of CASL semantics in terms of number of rules
The CASL language summary already clearly distinguishes between the mathematical concepts (underlying the language) and the language constructs themselves. This makes it possible that the definition of the semantics very closely follows the language summary. The complexity of the semantics of CASL is shown in Fig. 1. The semantics follows a natural semantics style and has both rules for static semantics (which are implemented by a static semantic checker) and model semantics (which are implemented by theorem-proving tools).