A large number of algebraic specification frameworks have been provided during the past 25 years of research, development, and applications in this area.Table X lists the main frameworks, with a rough indication of their chronology. Some of them are ambitious, wide-spectrum frameworks, equipped with a full software development methodology; others are much more modest, consisting essentially of a prototyping or verification tool and its associated language. For references and further details, see the COMPASS bibliography [BKL+91] and Recent Trends in Data Type Specification [HOD96].
Abel Etl Spectral Spectrum Lpg Extended-ML Obscure Troll 1990's Act-Two Asf+Sdf Rsl Asl Larch Rap SMoLCS Asspegique Cold-K 1980's Act-One Pluss Cip Obj Clear 1970's Look
Algebraic specification frameworks
No de-facto standard framework for algebraic specification has emerged.Although some of the existing frameworks are relatively popular, with substantial communities of users, none has achieved such widespread support as for example that enjoyed by VDM and Z in the model-oriented specification community. (The fact that VDM and Z have a lot of minor dialects is beside the point.) Most algebraic frameworks were developed at particular university departments, or by international collaboration between individual researchers, and each framework tends to be used rather locally. The main exceptions are LARCH and OBJ; one might mention here also ACT-ONE/TWO, RSL, and SPECTRUM. Not surprisingly, it seems that most frameworks strongly reflect the convictions held by their originators, which tends to make them less acceptable to those holding different convictions.
The lack of a common, widely-supported framework for algebraic specification is a major problem.In particular, it is an obstacle for the adoption of algebraic methods for use in industrial contexts, and makes it difficult to exploit standard examples, case studies and educational material. But even within academia, the diversity of explanations of basic algebraic specification notions in text-books, and the lack of a common corpus of accepted examples, form a significant hindrance to dissemination. And the various tools that have been developed for prototyping, verifying, and otherwise supporting the use of algebraic specifications, are each generally available only in connection with just one framework. Moreover, the prospects for continued support and development of locally-developed frameworks are usually quite uncertain, which discourages their adoption by industry and investment in training in their use.
It is time to agree on the fundamental concepts and constructs that could form the basis of a common framework.The various groups working on algebraic specification frameworks have already had ample opportunity to develop and experiment with their own particular variations on the theme of algebraic specification. A substantial collective experience and expertise in the design and use of such frameworks has been accumulated. If we cannot agree now on what are the essential concepts and constructs, there would seem to be little grounds for belief that such agreement could ever be achieved.
This paper presents CoFI: The Common Framework Initiative for algebraic specification and development, explains the (tentative) design of CASL: The CoFI Algebraic Specification Language, and sketches plans for the future.The author is currently the overall coordinator of CoFI. It should be emphasized that the ideas presented below stem from a voluntary international collaboration involving many participants (see the Acknowledgements at the end), and it would be both difficult and inappropriate to accredit particular ideas to individuals.
By the way: CoFI is intended to be pronounced like `coffee', and CASL like `castle'.
All the main points in this paper are summarized like this.The paragraphs following each point provide details and supplementary explanation. To get a quick overview of CoFI and CASL, simply read the main points and skip the intervening text. It is hoped that the display of the main points does not unduly hinder a continuous reading of the full text. (This style of presentation is borrowed from a book by Alexander [Ale79], where it is used with great effect.)