[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 ebm-vol-inv
enrich
   error-class
, 
   avolume, 
   nat-div
, 
   eraseblock
, 
   nat-set

with
   

   
   
   
   predicates  ebm-vol-inv : avolume;
               . ⊆ . : avolume × avolume;
   
   
   
   

   

   axioms ebm-vol-inv
          : ⊦   ebm-vol-inv(avol)
              ↔ (∀ n. n < # avol ∧ avol[n].mapped? → # avol[n].data ≤ LEB_SIZE ∧ is-aligned(# avol[n].data, EB_PAGE_SIZE));
          used for: ls;
          ebm-vol-le
          : ⊦   avol0 ⊆ avol1
              ↔   # avol0 = # avol1
                ∧ (∀ m. 
                       m < # avol0
                     →   (avol0[m].mapped? → avol1[m] = avol0[m])
                       ∧ (avol0[m] = unmapped ∧ avol1[m].mapped? → # avol1[m].data ≤ LEB_SIZE ∧ is-aligned(# avol1[m].data, EB_PAGE_SIZE)));
          used for: ls;

   

   
end enrich