[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 wbuf-base
enrich
   wbuf, 
   ebm-vol-inv
, 
   bufleb
with
   

   
   
   
   predicates  wbuf-cons : bufleb × wbuf × avolume × bool;
               wbuf-cons : wbuf × aleb × bool;
   
   variables  rofs : bool;
   
   

   

   axioms wbuf-cons-nobuf
          : ⊦   wbuf-cons(bleb, wbuf, avol, rofs)
              ↔ # wbuf.content = EB_PAGE_SIZE ∧ (bleb ≠ nobuffer → bleb.leb < # avol ∧ wbuf-cons(wbuf, avol[bleb.leb], rofs));
          used for: s, ls;
          wbuf-cons
          : ⊦   wbuf-cons(wbuf, aleb, rofs)
              ↔   aleb.mapped? ∧ wbuf.nbytes < # wbuf.content ∧ # wbuf.content = EB_PAGE_SIZE ∧ (¬ rofs → # aleb.data = wbuf.offset)
                ∧ (rofs → wbuf.offset ≤ # aleb.data) ∧ is-aligned(wbuf.offset, EB_PAGE_SIZE);
          used for: lws;

   

   
end enrich