A rationale for CoFI: The Common Framework Initiative, is given in a separate document [CoF97]. The present document focusses on the design of CASL, the main CoFI algebraic specification language.
By the way, the word `algebraic' is used in this document to refer to general axiomatic (property-oriented) specifications of classes of models. No restriction to equational logic is implied. Although the approach known as `algebraic specification' started from pure algebraic methods, which have especially good properties and constructions (e.g., initial models), and which are still useful, it can be advantageous to allow full first-order logic and (second-order) induction principles, for the sake of conciseness and clarity.
An early but key design decision was that the common framework should provide a coherent family of languages, all extensions or restrictions of some main algebraic specification language.Vital for the support for CoFI in the algebraic specification community is the coverage of concepts of many existing specification languages. How could this be achieved, without creating a complicated monster of a language? And how to avoid interminable conflicts with those needing a simpler language for use with prototyping and verification tools?
By providing not merely a single language but a coherent language family, CoFI allows the conflicting demands to be resolved, accommodating advanced as well as simpler languages. At the same time, this family is given a clear structure by being organized as restrictions and extensions of a main language, which is to be the main topic of the documentation (reference manual, user's guide, text book) and strongly identified with the common framework.
The main language of the common framework family is required to be competitive in expressiveness with various existing languages.The choice of concepts and constructs for the main language was a matter of finding a suitable balance point between the advanced and simpler languages. It was decided that its intended applicability should be for specifying the functional requirements and design of conventional software packages as abstract data types.
The tentative design of the main CoFI Algebraic Specification Language, called CASL, was completed in December 1996, and has since been investigated by task groups concerned with issues of language design, methodology, semantics, and tool support.On the basis of the investigations made by these groups, a definite complete proposal for the design of CASL [LD97a] has been submitted to IFIP WG 1.3 for approval at its meeting in June 1997.
See other documents for the abstract syntax and informal summary of CASL, concrete syntax examples, and a draft formal semantics.The CASL Summary [LD97b] provides an abstract syntax, together with an informal summary of the intended well-formedness conditions and semantics. The choice of preferred concrete syntax has not yet been made, but two proposals with examples are provided [KB97], [VBC97]. The formal semantics for (most of) the tentative design of CASL [LD96] is available [Sem97]; an updated draft of the formal semantics for the final proposed design is to be available at the IFIP WG 1.3 meeting.
CoFI is open to contributions and influence from all those working with algebraic specifications.The design of CASL was developed by a varying Language Design task group, coordinated by Bernd Krieg-Brückner, comprising between 10 and 20 active participants representing a broad range of algebraic specification approaches (the CoFI Rationale [CoF97] lists the names of all contributors to CoFI). Numerous study notes were written on various aspects of language design, and discussed at working and plenary language design meetings. The study notes and various drafts of the design summary were made available electronically and comments solicited via the associated mailing list (cofi-language@brics.dk). This document is based on part of a paper presented at TAPSOFT'97 [Mos97], explaining the tentative design of CASL [LD96].
The openness of the design effort should have removed any suspicion of undue bias towards constructs favoured by some particular `school' of algebraic specification. It is hoped that CASL incorporates just those features for which there is a wide consensus regarding their appropriateness, and that the common framework will indeed be able to subsume many existing frameworks and be seen as an attractive basis for future development and research--with high potential for strong collaboration.