1 Introduction

CASL is an expressive language for the algebraic specification of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). This paper presents CASL for users of the CafeOBJ framework.

CASL is intended as the main language of a coherent family of languages.

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 CASL 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 structure by being organized largely as restrictions and extensions of CASL.

Restrictions of CASL [Mos97][Mos98] correspond closely to languages used with existing tools for rapid prototyping, verification, term rewriting, etc. Extensions to CASL are to support various programming paradigms, e.g., object-oriented, higher-order [HKBM98], reactive.

A specification framework is more than just a language.

Apart from the CASL family of languages, the common framework is also to provide an associated development methodology, training materials, tool support, libraries, a reference manual, formal semantics and proof system, and conversion to and from other specification languages.

CASL is required to be competitive in expressiveness with various existing languages.

The choice of concepts and constructs for CASL was a matter of finding a suitable balance point between advanced and simpler languages, taking into account its intended applicability: for specifying the functional requirements and design of conventional software packages as abstract data types.

The 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. Almost all CASL features may be found (in some form or other) in one or more of the main existing algebraic specification frameworks.

The CASL design has been tentatively approved by IFIP WG 1.3.

The design proposal for CASL [LD97b] was submitted to IFIP Working Group 1.3 (Foundations of System Specification) in May 1997. The proposal provided the abstract syntax of the proposed language, together with an informal summary of the intended well-formedness conditions and semantics [LD97e]; the choice of concrete syntax had not been finalized. Accompanying documents gave the rationale for CoFI [CoF97] and for the CASL design [LD97c], and a draft formal semantics for CASL [Sem97].

The design was tentatively approved at the IFIP WG 1.3 meeting in Tarquinia, June 1997, subject to reconsideration of some particular points [LD97a] and the development of a satisfactory concrete syntax, both of which have now been completed [LD97d]. As a final check on the language design, the formal semantics is currently being updated to the final version. Tools and methodology for CASL are being developed; four prototype parsers, a well-formedness checker, and an interface to Isabelle have already been implemented.

CoFI is open to contributions and influence from all those working with algebraic specifications.

The design of CASL has been 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 have been 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 discussed on the language design mailing list (cofi-language@brics.dk).

The openness of the design effort should have removed any suspicion of undue bias towards constructs favoured by some narrow `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.

So much for the background of CASL.

Readers of this paper are assumed to be familiar with the CafeOBJ language and system.

For an introduction to CafeOBJ, see the CafeOBJ Report [DF98].

It should be stressed that the aims of CoFI (above) are quite different from those of the CafeOBJ project:

CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.
The CafeOBJ Home Page

There is however no direct support in CASL for the "new paradigms" of rewriting logic and hidden algebra. This is partly because these paradigms are not yet regarded as main-stream algebraic concepts, partly because they were felt to be somewhat too advanced for inclusion in a general-purpose specification language. CASL aims at reflecting the state-of-the-art of about five years ago, and leaves more recent advances to its extensions, which are also expected to provide support for particular paradigms such as object orientation and concurrency. In the case of hidden algebra, however, the intention is rather to provide the necessary methodological support by means of a notion of behavioural refinement, external to the CASL family of languages [BST96].

Moreover, in contrast to CafeOBJ, CASL itself is intended primarily as a specification language, not as a programming language. While rapid prototyping of CASL specifications may well be possible, and various executable sub-languages of CASL are to be provided, the constructs of CASL have been selected on the grounds of their expressiveness and semantic simplicity, without regard to their implementability.

In the CASL methodology, it is seen as an advantage that one can express requirements independently of executability concerns, thereby gaining clarity and being closer to informal requirements. As Amir Pnueli put it in his invited talk at ETAPS'98: requirement specifications and programs are two different views that should be checked (and debugged) against each other.

A deeper analysis of the interplay between methodology and language design, with reference to CafeOBJ and CASL, is given in an appendix.

With their stated differences of aims, it is only to be expected that there would be some substantial differences between the design of CafeOBJ and that of CASL. The purpose of this paper is to explain both the similarities and differences--addressing primarily readers who are already familiar with CafeOBJ.