5.3 Enumeration Declarations

The syntax of enumeration declarations is as in C++ (see Section r.7.2 of [Stroustrup91]).

enum-specifier ::= enum [ identifier ] { [ enumerator-definition-list ] }
enumerator-definition-list ::= enumerator-definition [ , enumerator-definition ] ...
enumerator-definition ::= identifier [ constant-initializer ]

See section 7.2 Class Member Specifications for the syntax of constant-initializer. The constant-expressions used in constant-initializers must be of an integral sort or the sort of some other enumerator [section 7.2, ANSI95].

The identifiers in an enumerator-definition are called enumerators. As in C++, the enumerators are constants in Larch/C++. If the identifier is used in the declaration of an enum-specifier, then the sort of the enumerators is that identifier, otherwise a unique sort name is generated for them. These new constants only have equal abstract values if they are defined with the same initializers (either explicitly or implicitly). For example, in the following:

enum color { red, orange, yellow, green, blue, indigo, violet=5 };
enum day_of_week { sun=1, mon, tues, wed, thurs, fri, sat };

the enumerators indigo and violet are equal. However, neither of them is equal to thurs, although they have the same values when converted to integers in C++ (see Section r.7.2 of [Stroustrup91]).

By using the trait function to_int, an enumerator can be converted to its integer value. With the above example, to_int(blue) has value 4 and sort int, whereas blue has sort color.

For example, the trait for the color example above would be the following. See section 11.1 Integer Types for the trait int.

% @(#)$Id: color_Trait.lsl,v 1.6 1997/06/03 20:29:59 leavens Exp $
color_Trait: trait
  includes int, NoContainedObjects(color)
  introduces
    red, orange, yellow, green, blue, indigo, violet: -> color
    to_int: color -> int

  asserts
    color generated by red, orange, yellow, green, blue, indigo, violet
    color partitioned by to_int: color -> int
    equations
      to_int(red) == 0;
      to_int(orange) == 1;
      to_int(yellow) == 2;
      to_int(green) == 3;
      to_int(blue) == 4;
      to_int(indigo) == 5;
      to_int(violet) == 5;

  implies
    \forall c1, c2: color
      (c1 = c2) == (to_int(c1) = to_int(c2))
    converts to_int: color -> int

The LSL enumeration of shorthand (see page 49 of [Guttag-Horning93]) is not used in the general construction of such traits. However, in many examples it could be combined with the Handbook trait Enumeration (see page 165 of [Guttag-Horning93]) and some renamings to construct an equivalent trait.

See section 11.6 Enumeration Types for the trait constructed for the day_of_week example.

The trait corresponding to an enumeration declaration is implicitly used in any specification module in which the declaration appears. (See section 2.7 Types and Sorts for more details on using a trait in a specification.)

Go to the first, previous, next, last section, table of contents.