
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
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 nonconstant operators. The distinction between constant and nonconstant 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:
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 SDL88 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
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 SDL88 and SDL92, properties can be specified more generally in SDL, but for historical reasons the keyword AXIOMS has been kept. 
Contact the webmaster with
questions or comments about this web site. 