[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-abs
enrich
   awbuf-inv, 
   wbuf-base
with
   

   
   
   functions  abs⊕ : aleb × wbuf → aleb;
   predicates  abs : avolume × bufleb × wbuf × avolume × bool;
   
   variables  rofs : bool;
   
   

   

   axioms abs-buf-leb-def :  ⊦ abs⊕(mapped(buf), wbuf) = mapped(buf + subarray(wbuf.content, 0, wbuf.nbytes));
          used for: s, ls;
          abs-buf-leb-unmapped :  ⊦ abs⊕(unmapped, wbuf) = unmapped;
          used for: s, ls;
          abs-def
          : ⊦   abs(avol0, bleb, wbuf, avol1, rofs)
              ↔   # avol0 = # avol1
                ∧ (∀ n. 
                       n < # avol0
                     →   (buffered(n) ≠ bleb → avol0[n] = avol1[n]) ∧ (¬ rofs ∧ buffered(n) = bleb → avol0[n] = abs⊕(avol1[n], wbuf))
                       ∧ (  rofs ∧ buffered(n) = bleb
                          →   wbuf.offset = # avol1[n].data ∧ avol0[n] = abs⊕(avol1[n], wbuf)
                            ∨   wbuf.offset < # avol1[n].data ∧ wbuf.offset + wbuf.nbytes < # avol1[n].data ∧ avol0[n] = avol1[n]
                              ∧ subarray(wbuf.content, 0, wbuf.nbytes) = subarray(avol1[n].data, wbuf.offset, wbuf.nbytes)));
          used for: ls;

   

   
end enrich