[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-base
enrich
   error-class
, 
   abstract-volumes
, 
   eraseblock
, 
   align

with
   

   
   
   
   predicates  . ⊆ . : abstract-volumes × abstract-volumes;
               ebm-initial : abstract-volumes;
               ebm-cons : abstract-volumes;
               ebm-cons : abstract-volume;
               valid-leb : leb;
   
   
   
   

   

   axioms erased-fill :  ⊦ erased.fill = 0;
          used for: s, ls;
          unmapped-fill :  ⊦ unmapped.fill = 0;
          used for: s, ls;
          ebm-initial :  ⊦ ebm-initial(avols) ↔ avols = ∅;
          used for: s, ls;
          ebm-cons :  ⊦ ebm-cons(evol) ↔ (∀ m. m < # evol → valid-leb(evol[m]));
          used for: ls;
          ebm-cons-def :  ⊦ ebm-cons(avols) ↔ (∀ v. v ∈ avols → ebm-cons(avols[v]));
          used for: ls;
          valid-leb-def
          : ⊦   valid-leb(leb)
              ↔   leb.mapped?
                →   # leb.data = LEB_SIZE ∧ leb.fill ≤ LEB_SIZE ∧ is-aligned(leb.fill, EB_PAGE_SIZE)
                  ∧ range=(leb.data, leb.fill, emptyleb, 0, LEB_SIZE - leb.fill);
          used for: s, ls;
          ebm-le
          : ⊦   avols0 ⊆ avols1
              ↔ (∀ v. 
                     (v ∈ avols0 ↔ v ∈ avols1)
                   ∧ (  v ∈ avols0
                      →   # avols0[v] = # avols1[v]
                        ∧ (∀ m. 
                               m < # avols0[v] ∧ avols0[v][m] ≠ unmapped
                             → (avols0[v][m] = erased → avols1[v][m] = erased) ∧ (avols0[v][m].mapped? → avols1[v][m] = avols0[v][m]))));
          used for: ls;

   

   
end enrich