Go backward to Background
Go up to Top
Go forward to CASL

CoFI

The initial idea for a common framework initiative was conceived in June 1994, by members of COMPASS and IFIP WG 1.3.

COMPASS (1989-96) was an ESPRIT Basic Research WG (3264, 6112) involving the vast majority of the European sites working on algebraic specification [KB96]. IFIP WG 1.3 (Foundations of System Specification) was founded in 1992 (originally with the number 14.3) and has members not only from the major European sites but also from other continents.

In fact the idea of developing a common algebraic specification framework had been suggested for inclusion in the original COMPASS WG proposal in 1988--but subsequently dropped, as it was considered unlikely to be achievable. By 1994, however, the area had matured sufficiently to encourage reconsideration of the idea of a common framework.

By September 1995 the main aims had been clarified, and CoFI: The Common Framework Initiative started.

A joint meeting of COMPASS and IFIP WG 1.3 at Soria Moria, near Oslo, in September 1995 decided to set up the Common Framework Initiative, and various task groups were formed. Since the termination of COMPASS in April 1996, IFIP WG 1.3 has taken the sole responsibility for the future of the initiative, and for approving any proposals that it might make.

The overall aims of CoFI [Mos96] are:

A common framework for algebraic specification and software development is to be designed, developed, and disseminated.
The production of the common framework is to be a collaborative effort, involving a large number of experts (30-50) from many different groups (20-30) working on algebraic specifications.
In the short term (e.g., by 1997) the common framework is to become accepted as an appropriate basis for a significant proportion of the research and development in algebraic specification.
Specifications in the common framework are to have a uniform, user-friendly syntax and straightforward semantics.
The common framework is to be able to replace many existing algebraic specification frameworks.
The common framework is to be supported by concise reference manuals, users' guides, libraries of specifications, tools, and educational materials.
In the longer term, the common framework is to be made attractive for use in industrial contexts.
The common framework is to be available free of charge, both to academic institutions and to industrial companies. It is to be protected against appropriation.

The common framework is to allow and be useful for:

Algebraic specification of the functional requirements of software systems, for some significant class of software systems.
Formal development of design specifications from requirements specifications, using some particular methods.
Documenting the relation between informal statements of requirements and formal specifications.
Verification of correctness of development steps from (formal) requirements to design specifications.
Documenting the relation between design specifications and implementations in software.
Exploration of the (logical) consequences of specifications: e.g., rewriting, theorem-proving, prototyping.
Reuse of parts of specifications.
Adjustment of specifications and developments to changes in requirements.
Providing a library of useful specification modules.
Providing a workbench of tools supporting the above.

In effect, the above list is the requirements specification for the common framework, avoiding premature design decisions. It provided the starting-point for the actual design of the common framework.

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.

(Sorry, no picture yet!)

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.

Restrictions of the main language are to correspond to languages used with existing tools for rapid prototyping, verification, term rewriting, etc.

These may be syntactic and/or semantic restrictions. The restricted languages need not have a common kernel--although presumably all restrictions will allow at least unstructured, single- or many-sorted equational specifications.

Existing tools typically restrict the use of sorts and overloading, allow only a restricted class of axioms, and may require specifications to be `flattened'.

The semantics of a specification in a restricted language may be inherited from the semantics of the main language, although some simplifications should usually be possible.

Extensions to the main language are to support various programming paradigms, e.g., object-oriented, higher-order, reactive.

These are to be obtained from the main language (or perhaps from mildly restricted languages) by syntactic and/or semantic extensions. The extended languages need not have a common super-language, and indeed, there may be technical difficulties in combining various extensions.

The semantics ascribed to a specification in the main language by an extension is required to be essentially the same as its original semantics.

The common framework is also to provide an associated development methodology, training materials, tool support, libraries, a reference manual, formal semantics, and conversion from existing frameworks.

A framework is more than just a language! Many existing algebraic specification frameworks have not had sufficient resources to develop all the required auxiliary documents, which has severely hampered their dissemination. By pooling resources in CoFI, this problem may be avoided.

Regarding tools, the aim is to make it possible to exploit existing tools in connection with the common framework, using an interchange format [BCV96].

One of the attractions of having a common framework is to facilitate building up a library of useful specifications in a single language. Libraries of specifications have previously been proposed, but the variety of languages involved was always a problem.

Conversion from existing frameworks is vital, not only to be able to reuse existing specifications, but also to encourage users to migrate from their current favourite framework to the common framework.

The tentative design of the main CoFI Algebraic Specification Language, called CASL, was completed in December 1996, and is currently undergoing closer investigation by task groups concerned with issues of language design, methodology, semantics, and tool support.

It was felt that CoFI participants had sufficient collective expertise and experience of designing algebraic specification frameworks, and knowledge of existing frameworks, to allow the rapid development of a tentative design for CASL by selecting and combining familiar concepts and constructs. (In fact it turned out that collaborative design of a language was a good way of forcing the participants to understand each other's views in depth--more reliably than through the attendance of presentations at conferences.) But then it was felt essential to allow time for a closer study before finalizing the design, in case any infelicities had crept in. In particular, it should be checked that there are no inherent semantic problems with the chosen combination of constructs.

Some CoFI task group meetings are to be held just before this paper is presented at TAPSOFT'97. On the basis of the investigations made by these groups, a definite complete proposal for the design of CASL will be submitted to IFIP WG 1.3 for approval at its meeting in June 1997.

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

The tentative 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. 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 tentative design summary were made available electronically and comments solicited via the associated mailing list (cofi-language@brics.dk).

This 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.

All the CoFI task groups welcome new active participants. See the descriptions of the task groups on the CoFI WWW pages [Mos97], and contact the coordinators of the task groups directly.

CoFI Tentative Document: Mosses97TAPSOFT --TAPSOFT'97-- April 1997.
Comments to pdmosses@brics.dk