 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.    