6.6 Generators

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

In many applications there are sorts which only differ in minor aspects from other sorts, but which are basically constructed in a similar way. In this case a partial type description can be parameterised. Parameterised types are very useful if types like sets, fields or queues are used. A set is usually a set of element of a certain type. The properties of the set are fairly independent of the type of the elements it contains. Without the possibility of parameterisation, every set of elements of a certain type has to be specified separately.

The following example is a partial type description for a set containing integer numbers. Integer is a predefined sort in SDL.

NEWTYPE int_set
LITERALS empty_int_set;
OPERATORS
        add:      int_set, Integer -> int_set;
        is_in:    int_set, Integer -> Boolean;
AXIOMS
FOR ALL m, n IN Integer, s IN int_set
        (is_in (empty_int_set, m) == false;
        is_in (add (s, m), n) == (m = n) OR (is_in (s, n));
        m=n è add (add (s, m), n) == add (s, m);
        m/=n è add (add (s, m), n) == add (add (s, n), m););
ENDNEWTYPE:

Sets can be formed with other types of elements, but the basic construction of the set is the same

NEWTYPE real_set
LITERALS empty_real_set;
OPERATORS
        add:       real_set, Real -> real_set;
        is_in:    real_set, Real -> Boolean;
AXIOMS
FOR ALL m, n IN Real, s IN real_set
        (is_in (empty_real_set, m) == false;
        is_in (add (s, m), n) == (m = n) OR (is_in (s, n));
        m=n è add (add (s, m), n) == add (s, m);
        m/=n è add (add (s, m), n) == add (add (s, n), m););
ENDNEWTYPE;

Obviously, these two descriptions above are almost identical and only differ in the “imported” sorts Integer or Real. To avoid repetition of text, the user can define a class of parameterised sorts by using the generator construct of SDL.

GENERATOR set
    (TYPE element, LITERALS empty_set)
LITERALS empty_set;
OPERATORS
        add:      set, element -> set;
        is_in:    set, element -> Boolean;
AXIOMS
FOR ALL m, n IN element, s IN set
        (is_in (empty_set, m) == false;
        is_in (add (s, m), n) == (m = n) OR (is_in (s, n));
        m=n è add (add (s, m), n) == add (s, m);
        m/=n è add (add (s, m), n) == add (add (s, n), m););
ENDGENERATOR;

The description is supplied with the formal parameter element now and can be actualized with any sort

NEWTYPE int_set set (Integer, empty_int_set)
ENDNEWTYPE;

NEWTYPE real_set set (real, empty_real_set)
ENDNEWTYPE;

Note: In SDL-92, parameterised types were introduced in general, but for data types the GENERATOR construct was retained. However, in SDL-2000, the parameterisation of all types was harmonised, and therefore the specific GENERATOR construct for data types was dropped.