Énumérations

TYPE enumeration{$s: identifier}
  -- Example: traffic_signal = enumeration{red, yellow, green}.
  INHERIT equality{enumeration{$s}}
  INHERIT total_order{enumeration{$s}}
  IMPORT identifier FROM field_names  -- See Appendix C.

  MODEL(code: nat)
    -- Position numbers in the generic parameter list.
  INVARIANT ALL(c: enumeration{$s} :: 1 <= c.code <= length(s))

  MESSAGE create(n: nat)
      -- Literal #s[k] = create(k), e.g. #yellow = create(2).
    WHEN 1 <= n <= length(s)
      REPLY(c: enumeration{$s}) WHERE c.code = n
    OTHERWISE REPLY EXCEPTION illegal_code

  MESSAGE ordinal(e: enumeration{$s}) REPLY(n: nat)
    WHERE n = c.code

  MESSAGE equal(e1 e2: enumeration{$s}) REPLY(b: boolean)
    WHERE b <=> (e1.code = e2.code)

  MESSAGE "<"(e1 e2: enumeration{$s}) REPLY(b: boolean)
    WHERE b <=> (e1.code < e2.code)
END