[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,

Specification Hashset-refines-Set-Theory-Instance
enrich
   Set-Test-IOAut, 
   Hashset-refines-Set, 
   IOforward-is-leqrefine

with
   constants 
       HashsetIOA : IOAutomaton(HashsetState, HashsetAction, EAction);
   
   functions 
       hashsetExt : HashsetAction → Opt(EAction);
   
   variables 
       tid : Tid;
       b : Bool;
       e : Elem;
       cs : HashsetState;
       as : SetState;
       gs : HashsetGState;
       ags : SetGState;
       lsf : Tid → HashsetLState;
       alsf : Tid → SetLState;
       ls : HashsetLState;
       als : SetLState;
       pcf : Tid → HashsetPC;
       apcf : Tid → SetPC;
       pc : HashsetPC;
       apc : SetPC;
   
   
   axioms 
      HashsetIOA-def: HashsetIOA = IOAut(hashsetInit, hashsetStep, hashsetExt);
      used for: s, ls;
      
      ext-DoInsert: hashsetExt(doINSERT(tid, b)) = τ;
      used for: s, ls;
      
      ext-DoMember: hashsetExt(doMEMBER(tid)) = τ;
      used for: s, ls;
      
      ext-InvInsert: hashsetExt(invINSERT(tid, e)) = ⌜InvInsert(tid, e)⌝ ;
      used for: s, ls;
      
      ext-RetInsert: hashsetExt(retINSERT(tid, b)) = ⌜RetInsert(tid, b)⌝ ;
      used for: s, ls;
      
      ext-InvMember: hashsetExt(invMEMBER(tid, e)) = ⌜InvMember(tid, e)⌝ ;
      used for: s, ls;
      
      ext-RetMember: hashsetExt(retMEMBER(tid, b)) = ⌜RetMember(tid, b)⌝ ;
      used for: s, ls;
      
      ext-tau: hashsetExt(τ) = τ;
      used for: s, ls;
   
   theorems 
      abs-is-fwsim: fwsim(HashsetIOA, SetIOA, λ as, cs. abs(cs, as) ∧ SetInv(as.gstate, as.lsf, as.pcf) ∧ HashsetInv(cs.gstate, cs.lsf, cs.pcf));
      
      Hashset-fwsim-Set: ≤F(HashsetIOA, SetIOA);
      
      Hashset-refines-Set: C_≤T_A(HashsetIOA, SetIOA);
   
   
end enrich