11.6 Enumeration Types

The abstract values of an enumeration type in C++ are given by a trait constructed according to that type's declaration (see section 5.3 Enumeration Declarations).

For example, consider the following declaration.

enum day_of_week { sun=1, mon, tues, wed, thurs, fri, sat };

The trait for the day_of_week example would be as follows. See section 11.1 Integer Types for the trait int.

% @(#)$Id: day_of_week_Trait.lsl,v 1.6 1997/06/03 20:29:59 leavens Exp $
day_of_week_Trait: trait
  includes int, NoContainedObjects(day_of_week)
  introduces
    sun, mon, tues, wed, thurs, fri, sat: -> day_of_week
    to_int: day_of_week -> int

  asserts
    day_of_week generated by sun, mon, tues, wed, thurs, fri, sat
    day_of_week partitioned by to_int: day_of_week -> int
    equations
      to_int(sun) == 1;
      to_int(mon) == 2;
      to_int(tues) == 3;
      to_int(wed) == 4;
      to_int(thurs) == 5;
      to_int(fri) == 6;
      to_int(sat) == 7;

  implies
    \forall d1, d2: day_of_week
      (d1 = d2) == (to_int(d1) = to_int(d2))
      converts to_int: day_of_week -> int

The trait corresponding to an enumeration declaration is implicitly used in any specification module in which the declaration appears. For example, the trait day_of_week_Trait would be used in the module in which the declaration of day_of_week 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.