6.2 Partial type definitions

Tutorial on SDL-88
Belina, Hogrefe (edits Reed)

With a partial type definition a user always specifies exactly one sort. The definition is introduced by the keyword NEWTYPE and is finished with ENDNEWTYPE. First the sortname is specified

NEWTYPE sortname
. . .
ENDNEWTYPE;

The keyword LITERALS introduces constants: that is, operators without parameters (the keyword CONSTANT is used for different purpose). The keyword OPERATORS is followed by the definition of the signatures of non-constant operators. The distinction between constant and non-constant operators is probably intuitive for someone not familiar with ADTs and has practical reasons, but in the underlying algebra they are both operators and LOTOS (for example) does not distinguish between these.

The definition of equations follows the keyword AXIOMS. The partial type definition for the ADT of in Introduction to ADT then looks like the following:

NEWTYPE Bool
LITERALS true, false;
OPERATORS
        not: Bool -> Bool;
AXIOMS
        not (true) = false;
        not (false) = true;
ENDNEWTYPE Bool:

NEWTYPE Nat
LITERALS 0,1
OPERATORS
        plus : Nat, Nat -> Nat;
        isZero : Nat -> Bool
AXIOMS
FOR ALL x, y IN Nat
        (plus (x, y) == plus (y, x);
        plus (x, 0) == x;
        plus (x, plus (y, 1) == plus (plus (x, y), 1 );
        isZero (0) == true;
        isZero (plus (x, 1)) == false;);
ENDNEWTYPE Nat;

The two partial type definittions above together define implicitly the ADT example of "Construction of a sort by the use of equations". The names of the sorts are capitalised here: this is not required (moreover in SDL-88 the case of names is ignored so that Ab is the same as aB), but by convention sort names start with a capital letter.

The "==" notation is used to distinguish equivalence from Boolean equality operator, which is denoted "=". The Boolean equality is always defined implicitly together with the Boolean inequality "/=" for every sort (such Nat), and has the usual properties.

The keyword AXIOMS has historical reasons. The word "axiom" is usually used for very specific equations. In practice frequently, an equation of the form

term == true

is used. If the "== true"-part is omitted, one is talking about an axiom. In earlier versions of SDL, all properties of a sort were specified by just using this kind of equations. In SDL-88 and SDL-92, properties can be specified more generally in SDL, but for historical reasons the keyword AXIOMS has been kept.