Caractères

TYPE char
  INHERIT equality{char}
  INHERIT total_order{char}

  MODEL(code: nat)  -- ASCII codes.
  INVARIANT ALL(c: char :: 0 <= c.code <= 127)

  MESSAGE create(n: nat)  -- literal 'a' = create(97) and so on.
    WHEN 0 <= n <= 127 REPLY(c: char) WHERE c.code = n
    OTHERWISE REPLY EXCEPTION illegal_code

  MESSAGE ordinal(c: char) REPLY(n: nat)
    WHERE n = c.code

  MESSAGE equal(c1 c2: char) REPLY(b: boolean)
    WHERE b <=> (c1.code = c2.code)

  MESSAGE "<"(c1 c2: char) REPLY(b: boolean)
    WHERE b <=> (c1.code < c2.code)

  CONCEPT letter(c: char) VALUE(b: boolean)
    WHERE b <=> (c IN ['a' .. 'z'] | c IN ['A' .. 'Z'])

  CONCEPT digit(c: char) VALUE(b: boolean)
    WHERE b <=> c IN ['0' .. '9']
END