Go up to Top
Go forward to 2 CASL and its semantics

1 Introduction

During the past decades a large number of algebraic specification languages have been developed. Unfortunately, these languages are based on a diversity of basic algebraic specification concepts. The presence of so many similar specification languages with no common framework had hindered the dissemination and application of research results in algebraic specification. In particular, it had made it difficult to produce educational material, to re-use tools and to get algebraic methods adopted in industry. Therefore, in 1995, an initiative, CoFI¹, to design a Common Framework for Algebraic Specification and Development was started [Mos97]. The goal of CoFI is to get a common agreement in the algebraic specification community about basic concepts, and to provide a family of specification languages at different levels, a development methodology and tool support. The family of specification languages comprises of a central, common language, called CASL², various restrictions of CASL, and various extensions of CASL (e.g. with facilities for particular programming paradigms).

The definition of CASL and some of its sublanguages has been finished [CoF98]. Moreover, a complete formal semantics of CASL [CoF99] has been developed in parallel with design of the language and indeed, the development of the semantics has given important feedback to the language design.

Now that design and semantics of CASL have been finished, it is essential to have a good tool support. Tools will be essential for the goal of CoFI to get CASL accepted in academic communities (in the short run), and, in the long run, in industry. This holds even stronger since CASL is a language with a formal semantics: many people believe that such a language cannot or will not be used in practice: "The best semantics will not win." [Lar99]

Since CASL was designed with the goal to subsume many previous frameworks, it has become a powerful and quite complex language. This complexity makes it harder to build tools covering the whole language.

In this work, we will show that it is possible to build tools for a complex language with strong semantics in a reasonable time. In order to achieve this, we have followed several guidelines:

As much as possible, re-use existing tools, instead of building new ones.
Build tools in such a way that tools developed at different sites can be integrated; thus, not every site has to develop all the tools.
Make tools as generic as possible. After all, CASL only is the central language in a whole family of languages, and it would be tedious to have to re-implement the same things for each language separately.

All these guidelines are even more important in a non-commercial environment as the CoFI initiative is, where only very limited (wo)man-power is available, and therefore collaborative effort is essential. Moreover, an explicit goal within the design of CASL was to provide a common language in order to achieve a better interoperability of (already existing) tools.

We will discuss these guidelines, reporting how well they work in practice and which difficulties arise with them.

The paper is organized as follows:

Section 2 gives a brief overview over CASL and its semantics. Section 3 explains the general architecture of the Bremen HOL-CASL tool. In section 4, tool interoperability using a common interchange format is discussed. Section 5 describes the problems with parsing CASL's mixfix syntax. Section 6 recalls the encoding of CASL in higher-order logic from [MKK98], while section 7 reports our practical experiences when using this encoding to create an interface from CASL to Isabelle/HOL. Section 8 describes a way how to make the static analysis of CASL structured specifications independent of the underlying logic, which gives a generic tool that can be re-used for different logics. In section 9, some difficulties of encoding CASL structured specifications into Isabelle are discussed. Section 10 describes several user interfaces for HOL-CASL. Finally, section 11 contains conclusions and directions for future work.

This work is based on [MKK98], but considerably extends the work begun there.

CoFI Note: T-10 -- Version: v1.0 -- 10 Dec 1999.
Comments to till@informatik.uni-bremen.de