Specification cuckoo

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   table
with
   
   
   
   
   procedures lookup elem, table, table, elem → nat, elem → nat : bool  ;;
              insert elem, elem → nat, elem → nat : table, table nonfunctional ;;
              insert_rec elem, elem → nat, elem → nat : table, table nonfunctional ;;
   variables  h : elem → nat;
              h1 : elem → nat;
              h2 : elem → nat;
              found? : bool;

   

   

   

   declarations lookup : lookup(a, T1, T2, h1, h2; found?){found? := T1[h1(a)] = full(a) ∨ T2[h2(a)] = full(a)};
                insert-rec
                : insert_rec(a, h1, h2; T1, T2)
                  {let slot = T1[h1(a)] in {T1 := T1[h1(a), full(a)]; if slot ≠ empty then insert_rec(slot.elem, h2, h1; T2, T1)}}
                ;
                insert
                : insert(a, h1, h2; T1, T2)
                  {let found? = false
                   in {lookup(a, T1, T2, h1, h2; found?); 
                       while ¬ found?
                       do {if T1[h1(a)] = empty then {T1 := T1[h1(a), full(a)]; found? := true}; 
                           if ¬ found?
                           then {a := T1[h1(a)].elem, T1 := T1[h1(a), T1[h1(a)].elem:= a]; 
                                 if T2[h2(a)] = empty then {T2 := T2[h2(a), full(a)]; found? := true}}; 
                           if ¬ found? then a := T2[h2(a)].elem, T2 := T2[h2(a), T2[h2(a)].elem:= a]}}
                  }
                ;
end enrich