CoFI: The Common Framework Initiative
for Algebraic Specification and Development

Peter D. Mosses(2)

April 1997

This document is available for browsing on WWW as Hypertext, and for printing on A4 paper in Postscript and DVI formats.

Summary

An open collaborative effort has been initiated: to design a common framework for algebraic specification and development of software. The rationale behind this initiative is that the lack of such a common framework greatly hinders the dissemination and application of research results in algebraic specification. In particular, the proliferation of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread acceptance throughout the research community is urgently needed.

The aim is to base the common framework as much as possible on a critical selection of features that have already been explored in various contexts. The common framework will provide a family of specification languages at different levels: a central, reasonably expressive language, called CASL, for specifying (requirements, design, and architecture of) conventional software; restrictions of CASL to simpler languages, for use primarily in connection with prototyping and verification tools; and extensions of CASL, oriented towards particular programming paradigms, such as reactive systems and object-based systems. It should also be possible to embed many existing algebraic specification languages in members of the CASL family.

A tentative design for CASL has already been proposed. Task groups are studying its formal semantics, tool support, methodology, and other aspects, in preparation for the finalization of the design.

Contents

  • Background
  • CoFI
  • CASL
  • Basic Specifications
  • Partiality
  • Subsorts and Overloading
  • Formulae
  • Sort Generation Constraints
  • Structured Specifications
  • Translation and Hiding
  • Union and Extension
  • Initiality and Freeness
  • Type Definition Groups
  • Naming and Generics
  • Architectural Specifications
  • Libraries of Specifications
  • Foreground
  • Acknowledgements
  • References
  • Appendices:
  • Appendix: Tentative Abstract Syntax of CASL
  • Identifiers
  • Basic Specifications
  • Basic Specifications with Subsorts
  • Structured Specifications
  • Generic Specifications
  • Architectural Specifications
  • Specification Libraries
  • Footnotes
  • This document was converted from LaTeX2e sources to HTML using Hyperlatex 2.0.
    CoFI Tentative Document: Mosses97TAPSOFT --TAPSOFT'97-- April 1997.
    Comments to pdmosses@brics.dk