refTable.lsl

refTable(Ind, Val, Tab): trait
   includes Set(Ind, IndSet)
   introduces
      new: -> Tab
      assign: Tab, Ind, Val -> Tab
      delete: Tab, Ind -> Tab
      __[__]: Tab, Ind -> Val
      domain: Tab -> IndSet
      nil: -> Ind
      newInd: Ind, Tab, Tab -> Bool
   asserts
     Tab generated by new, assign
     Tab partitioned by __[__], domain
     \forall i, i1, i2: Ind, v: Val, t,t1,t2: Tab
       delete(new, i) == new;
       delete(assign(t, i1, v), i2) ==
          if i1 = i2
          then delete(t, i2)
          else assign(delete(t, i2), i1, v);
       assign(t, i1, v)[i2] ==
           if i1 = i2 then v else t[i2];
       domain(new) = {};
       domain(assign(t, i, v)) ==
           insert(i, domain(t));
       newInd(i, t1, t2) == ~(i \in domain(t1))
           /\ domain(t2) = insert(i, domain(t1))
           /\ ~(i = nil)