[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 Set-Test-IOAut
specification
   using Set-proofs, IOtrace
   data types 
      EAction = InvInsert(. .tid : Tid;. .e : Elem)
              | InvMember(. .tid : Tid;. .e : Elem)
              | RetInsert(. .tid : Tid;. .b : Bool)
              | RetMember(. .tid : Tid;. .b : Bool)
              ;
   
   variables 
       ea : EAction;
       tid : Tid;
       e : Elem;
       b : Bool;
   
   constants 
       SetIOA : IOAutomaton(SetState, SetAction, EAction);
   
   functions 
       setExt : SetAction → Opt(EAction);
   
   variables 
       ea : EAction;
       a : SetAction;
       tid : Tid;
       e : Elem;
       b : Bool;
       s : SetState;
       sl : List(SetState);
       al : List(SetAction);
       el : List(EAction);
       m : Nat;
       n : Nat;
       gstate : SetGState;
       lsf : Tid → SetLState;
       pcf : Tid → SetPC;
   
   
   axioms 
      SetIOA-def: SetIOA = IOAut(setInit, setStep, setExt);
      
      ext-DoInsert: setExt(ADoInsert(tid, b)) = τ;
      used for: s, ls;
      
      ext-DoMember: setExt(ADoMember(tid)) = τ;
      used for: s, ls;
      
      ext-InvInsert: setExt(AInvInsert(tid, e)) = ⌜InvInsert(tid, e)⌝ ;
      used for: s, ls;
      
      ext-RetInsert: setExt(ARetInsert(tid, b)) = ⌜RetInsert(tid, b)⌝ ;
      used for: s, ls;
      
      ext-InvMember: setExt(AInvMember(tid, e)) = ⌜InvMember(tid, e)⌝ ;
      used for: s, ls;
      
      ext-RetMember: setExt(ARetMember(tid, b)) = ⌜RetMember(tid, b)⌝ ;
      used for: s, ls;
   
   
end specification