N.B. A formatting mistake originally caused all the changed bits of the abstract syntax to be almost illegible in the versions formatted for printing! This has now been eliminated.
This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.
This Summary is the basis for the Design Proposal [LD97b] for CASL, the Common Algebraic Specification Language, prepared by the Language Design Task Group of CoFI, the Common Framework Initiative. It gives the abstract syntax, and informally describes its intended semantics. It is accompanied by the Rationale for CoFI [CoF97], the Rationale for the Proposed Design of CASL [LD97c], a draft of the Formal Semantics of CASL [Sem97c], and proposals for Concrete Syntax, with Examples of how CASL specifications might look [KB97][VBC97][Mos97a].Version 0.97 of the CASL Design Proposal was submitted for approval to the sponsoring IFIP Working Group on Foundations of System Specification, WG 1.3. It received tentative approval, together with a referees' report recommending the reconsideration of some elements of the design [IFI97]; a response has already been made [LD97a].
The present version of this Summary shows just which bits of CASL are currently subject to reconsideration or revision, in view of the referees' comments and the recommendations made by the CoFI Semantics Task Group [Sem97c]. Changes that were made since the previous version are highlighted in the same way as this sentence. Points where further discussion is required are highlighted like this sentence.
All comments on this Summary should be sent to the CoFI Language Design mailing list(
cofi-language@brics.dk).Deadline for comments to be considered at the Amsterdam Meeting of the Language Design Task Group:
12 noon on Tuesday, 23 September 1997.The language CASL 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. 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 conservative and/or free; initiality constraints are a special case. A simple form of generic 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.