ereftab.lsl

ereftab: trait
  assumes CTrait
  introduces
    empty: -> ereftab
    add: ereftab, employee, eref -> ereftab
    delete: ereftab, eref -> ereftab
    getERef: ereftab, employee -> eref
    erefNIL: -> eref
    in: ereftab, eref -> bool
    size: ereftab -> int
  asserts
    ereftab generated by empty, add
    ereftab partitioned by getERef
    \forall e, e1: employee, er, er1: eref, t: ereftab
      delete(empty, er) == empty;
      delete(add(t, e, er), er1) ==
         if er = er1 then t
         else add(delete(t, er1), e, er);
      in(empty, er) == false;
      in(add(t, e, er), er1) == er = er1 \/ in(t, er);
      getERef(empty, e1) == erefNIL;
      getERef(add(t, e, er), e1) ==
         if e = e1 then er else getERef(t, e1);
      size(empty) == 0;
      size(add(t, e, er)) ==
         1 + (if in(t, er) then 0 else 1)