% Copyright (C) 1993 Digital Equipment Corporation
% All rights reserved.
% See the file COPYRIGHT for a full description. 
% Last modified on Fri Jun 18 17:04:03 PDT 1993 by horning

atom(At, Str, Tab): trait
  % Defines a table of atom, string pairs.
  includes hash(Str, Int)
  introduces
    new: -> Tab
    insert: Tab, At, Str -> Tab
    __\in __: Str, Tab -> Bool
    toText: At, Tab -> Str
  asserts 
    Tab generated by new, insert
    \forall a, a1, a2: At, s, s1, s2: Str, t: Tab

      ~(s \in new);
      s1 \in insert(t, a, s2) == s1 = s2 \/ s1 \in t;

      toText(a2, insert(t, a1, s)) ==
        if a1 = a2 then s else toText(a2, t)


      
