Scanner(T): trait
  includes Octet,
    Character,
    List(String, Character)
    Octet,
    List(Construct, Symbol),
    List(TextSeq, OctetSeq)

  introduces
     recognize: T, State, OctetSeq,
         SymbolSeq, TextSeq, State, OctetSeq -> Bool

     % for recognize(s, si, osi, ss, ts, so, oso), read:
     %  Scanner s, in state si, when presented
     %  with OctetSeq osi, recognizes Construct c
     %  (consisting of octet sequences ts),
     %  enters state so, and leaves oso remaining

     encoding: T -> Encoding

     % each scanner has an encoding, i.e. a mapping from
     % octet sequences to character sequences

     fsm: T, State -> FSM

     % A scanner is controlled by a set of finite state machines,
     % one for each of the scanner's states.

  asserts forall s:T, si,so: State, first,rest: OctetSeq,
      sym: Symbol, text: CharSeq, tokens: Construct

    recognize(s, si, empty, empty, empty, si, empty)

    recognize(s, si, tokRep || constrestRep || rest,
              sym \precat syms, text \precat texts, so, rest) =>
      accept(fsm(s, si), encoding(s)[tokRep]) /\
      @@@