This document is available for browsing on WWW as Hypertext, and for printing on A4 paper in Postscript and DVI formats.
This is the official summary of the Tentative Design of CASL, the CoFI Algebraic Specification Language. Please take a close look at it, and report any mistakes or inconsistencies that you notice, as well as pointing out any parts that still need further clarification (bearing in mind the informal nature of this summary). All comments on the Tentative Design of CASL and on this summary should be sent to the CoFI Language Design mailing list (cofi-language@brics.dk).This document will be the basis for closer investigation of the tentative language design by various CoFI task groups (Semantics, Tools, Methodology, Language Design), leading to a firm CASL Design Proposal in March 1997.
The language CASL summarized here is central to CoFI: it is a reasonably expressive algebraic language for specifying requirements and design for conventional software. From CASL, simpler CoFI languages (e.g., for interfacing with existing tools) are to be obtained by restriction, and CASL is to be incorporated in more advanced CoFI languages (e.g., for specifying reactive systems). CASL strikes a balance between simplicity and expressiveness. The main features of its design are as follows:
Many-sorted basic specifications in CASL denote classes of many-sorted partial first-order structures: algebras where the functions are partial or total, and where also predicates are allowed. Axioms are first-order formulae built from definedness assertions and both strong and existential equations. Sort generation constraints can be stated. Type definitions are provided for concise specification of enumerations and products. Subsorted basic specifications provide moreover a simple treatment of subsorts, interpreting them as embeddings.
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. 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.
For further details of the original requirements and functionality for the CoFI Common Language for Algebraic Specification, see the Working Documents "Meta-Requirements" and "Meta-Design", accessible via the CoFI Home Page.