[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 FLITPSCweak-preds
enrich
   FLITPSC-preds
with
   functions 
       firstPersistW : List(FOW) → Nat;
   
   predicates 
       . ⊒W . : List(FOW) × List(FOW);
       rely : T × List(FOW) × List(FOW);
       rely : T × (L → List(FOW)) × (L → List(FOW));
       isPersistFO : Nat × List(FOW);
   
   variables 
       ctr : L → Nat;
       p : L → List(FOW);
       l : L;
       fowl : List(FOW);
       fow : FOW;
       t : T;
       ts : Set(T);
       tsf : L → Set(T);
       writers : L → Set(T);
       readers : L → Set(T);
       n : Nat;
       m : Nat;
       v : V;
       mem : L → V;
   
   
   axioms 
      firstPersistW: firstPersistW(fowl) = fowl.indexWhere(.W?);
      used for: ls;
      
      isPersistFO: isPersistFO(n, fowl) ↔ n < # fowl ∧ fowl[n].FO? ∧ (∀ m. m < n → fowl[m].tid ≠ fowl[n].tid ∧ fowl[m].FO?);
      used for: ls;
      
      weak-write-postfix: fowl0 ⊒W fowl1 ↔ (∃ fowl2, fowl3, fowl4, fowl5. fowl0 = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4);
      used for: ls;
      
      allrely-def: rely(t, p, p0) ↔ (∀ l. rely(t, p(l), p0(l)));
      used for: ls;
      
      rely-def: rely(t, fowl, fowl0) ↔ (∃ fowl1, fowl2. fowl ⊒W fowl1 ∧ fowl0 = fowl1 + fowl2 ∧ fowl2 | t = []);
      used for: ls;
   
   
end enrich