Introduction

Introduction

The basic datatypes of [4] are written obeying the following methodological guidelines. We formulate them explicitly for several reasons:

Many design decisions in the basic datatypes make only sense in context of the guidelines.
The guidelines are useful in general for writing specifications in CASL.
The guidelines can serve as a starting point for a new set of methodological guidelines for other applications.

For the guidelines we adopt the style of the book "A Pattern Language" [1]. Reflecting the marking of [1], all of our guidelines should be marked with one asterisk. I.e. with the words of [1] we claim that "we have made some progress", "but with careful work it will certainly be possible to improve on the solution" - not astonishing, as these guidelines are the first "style-guide" how to write specifications in CASL.

If we had pointed out in the guidelines themselves that they are rules of thumb, we would have had to stress phrasings like "if possible", "if adequate", "whenever possible" too much. Thus we formulate them as general statements. Examples from the basic datatypes illustrate their use. The discussion of a guideline justifies the underlying design decision and - as there is no rule without a meaningful exception - shows its limitations.

At certain points, e.g. the naming scheme of axioms, this note differs from the current version 0.7 of the Basic Datatypes. The next revision of the Basic Datatypes will take care of all guidelines presented in this note.

We propose two new annotations in this note: %mono and %implied . Their purpose is explained on pages X and X, respectively. We freely use them throughout the note.

CoFI Note: M-6 -- Version: 0.7 -- June 2002.
Comments to cofi@informatik.uni-bremen.de

Introduction