[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 abs-FLITPSCweak-PLIB
enrich
   FLITPSCweak-proofs, 
   PLIB-proofs
with
   predicates 
       abs : List((RWevent, Bool)) × (L → Set(T)) × (L → List(FOW));
       absloc : List(RWevent) × Set(T) × List(FOW);
   
   variables 
       glb : Nat;
       loc : Nat;
       l : L;
       wl : L;
       il : L;
       ctr : L → Nat;
       p : L → List(FOW);
       fowl : List(FOW);
       ws : L → Set(T);
       mem : L → V;
       vm : L → V;
       pm : L → V;
       h : List((RWevent, Bool));
       v : V;
       iv : V;
       ov : V;
       t : T;
       tid : T;
       vpe : (RWevent, Bool);
       m : Nat;
       n : Nat;
       b : Bool;
       e : RWevent;
       el : List(RWevent);
       ags : PLIBGState;
       gs : FLITPSCGState;
       rs : L → Set(T);
       rset : Set(T);
       fow : FOW;
       persisted : L → Bool;
   
   
   axioms 
      abs-def: abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)));
      
      absloc-base: absloc([], rset, fowl) ↔ fowl |W = [];
      
      absloc-recW-empty: ¬ absloc(W(t, l, v) ' + el, rset, []);
      
      absloc-recW-FO: absloc(W(t, l, v) ' + el, rset, FO(t0) ' + fowl) ↔ absloc(W(t, l, v) ' + el, rset, fowl);
      
      absloc-recW-W: absloc(W(t, l, v) ' + el, rset, W(v0, t0) ' + fowl) ↔ t0 = t ∧ v0 = v ∧ absloc(el, rset, fowl);
      
      absloc-recR: absloc(R(t, l, v) ' + el, rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ absloc(el, rset, fowl);
   
   
end enrich