Symboles

TYPE symbol
  INHERIT equality{symbol}
  MODEL(name: string)
  INVARIANT ALL(s: symbol :: length(s.name) > 0)

  MESSAGE create(name: string)
    WHEN length(name) > 0
      REPLY(s: symbol) WHERE s.name = name
    OTHERWISE REPLY EXCEPTION empty_symbol

  MESSAGE equal(s1 s2: symbol)
    REPLY(b: boolean)
      WHERE b <=> s1.name = s2.name
END