This section presents the main points of the tentative design of CASL.
The tentative 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.
The tentative design of CASL provides the abstract syntax, together with an informal summary of the intended well-formedness conditions and semantics; the choice of concrete syntax has not yet been made.It is well-known that people can have strong feelings about issues of concrete syntax, and it was felt necessary to delay all discussions of such issues until after the tentative design of the CASL abstract syntax and its intended semantics had been decided. Consequently, CASL is at the time of writing without any concrete syntax at all, which makes it difficult to give accurate illustrative examples of specifications.
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. Structured specifications allow translation, reduction, union, and extension of specifications. Extensions may be required to be persistent and/or free; initiality constraints are a special case. Type definitions are provided for concise specification of enumerations and products. 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 tentative design choices that have been made. The complete tentative abstract syntax of CASL is given in an appendix. For a systematic presentation of the intended semantics of CASL constructs, see the CASL Tentative Design Summary [CoF96], available for browsing on WWW via the CoFI Home Page [Mos97].