The design of CASL is based on a critical selection of the concepts and constructs found in existing algebraic specification frameworks.The main novelty of CASL lies in its particular combination of concepts and constructs, rather than in the latter per se. All CASL features may be found (in some form or other) in one or more of the main existing algebraic specification frameworks, with a couple of minor exceptions: with subsorts, it was preferred to avoid the (non-modular) condition of `regularity'; and with libraries, it was felt necessary to cater for links to remote sites.
The aim with CASL is to provide an expressive specification language with simple semantics and good pragmatics.The reader may notice below that from a theoretical point of view, some CASL constructs could be eliminated, the same effect being obtainable by combined use of the remaining constructs. This is because CASL is not intended as a general kernel language with constructs that directly reflect theoretical foundations, and where one would need to rely on `syntactic sugar' to provide conciseness and practicality. By including abbreviatory constructs in the syntax of CASL, their uniformity with the rest of the syntax may be enforced, and in any case they add no significant complications at all to the CASL semantics.
CASL is for specifying requirements and design of conventional software packages.All CASL constructs are motivated by their usefulness in general algebraic specification: there are no special-purpose constructs, only for use in special applications, nor is CASL biased towards particular programming paradigms.
Let us consider the concepts and constructs of so-called basic specifications in CASL, followed by structured specifications, architectural specifications, and finally libraries of specifications.First, here is a concise overview of the complete language. Basic specifications in CASL denote classes of partial first-order structures: algebras where the functions are partial or total, and where also predicates are allowed. Subsorts are interpreted as embeddings. Axioms are first-order formulae built from definedness assertions and both strong and existential equations. Sort generation constraints can be stated. Datatype declarations are provided for concise specification of sorts equipped with some constructors and (optional) selectors, including enumerations and products. Structured specifications allow translation, reduction, union, and extension of specifications. Extensions may be required to be conservative and/or free; initiality constraints are a special case. A simple form of generic (parametrized) specifications is provided, together with instantiation involving parameter-fitting translations. Architectural specifications express that the specified software is to be composed from separately-developed, reusable units with clear interfaces. Finally, libraries allow the (distributed) storage and retrieval of named specifications.
The remarks below explain how CASL caters for the various features, and attempts to justify the design choices that have been made.