The formatted body and appendices of this document are also available separately.
A draft of this document has been discussed by the Language Design task group at its meeting in Lisbon and on the mailing list (see the archives). The editor has tried to take account of the points made in the discussions when producing this final version. N.B. None of the changes are marked in this document! For the benefit of those who have read the draft version, an alternative document is provided, with all significant changes marked; the formatting and pagination should be otherwise (almost) identical.Any complaints about changes that have (or have not) been made should be sent to the mailing list as soon as possible.
This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.
The language CASL is central to CoFI, the Common Framework Initiative for algebraic specification and development. It is a reasonably expressive algebraic language for specifying requirements and design for conventional software. From CASL, simpler languages (e.g., for interfacing with existing tools) are to be obtained by restriction, and CASL is to be incorporated in more advanced languages (e.g., higher-order). 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 equations and definedness assertions. Sort generation constraints can be stated. Datatype declarations are provided for concise specification of sorts together with some constructors and (optional) selectors. Subsorted basic specifications provide moreover a simple treatment of subsorts, interpreting subsort inclusion as embedding.
Structured specifications allow translation, reduction, union, and extension of specifications. Extensions may be required to be free; initiality constraints are a special case. A simple form of generic specifications is provided, together with instantiation involving parameter-fitting translations and views.
Architectural specifications express that the specified software is to be composed from separately-developed, reusable units with clear interfaces.
Finally, specification libraries allow the (distributed) storage and retrieval of named specifications.
This document gives a detailed summary of the syntax and intended semantics of CASL. It is intended for readers who are already familiar with the main concepts of algebraic specifications.