[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 ubi-io-abs
enrich
   ubi-io-inv, 
   ubi-io-base, 
   encoding-echeader
, 
   encoding-vidheader
, 
   aecheader, 
   avidheader, 
   mtd-base

with
   

   
   
   functions  initial-apebs : pebs → apebs;
   predicates  abs : pebs × apebs;
               abs-peb : peb × apeb;
               abs-echdr : buffer × aecheader;
               abs-vidhdr : buffer × avidheader;
   
   
   
   

   

   axioms abs :  ⊦ abs(pebs, apebs) ↔ # pebs = # apebs ∧ (∀ n. n < # pebs → abs-peb(pebs[n], apebs[n]));
          used for: ls;
          abs-peb
          : ⊦   abs-peb(peb, apeb)
              ↔   (peb.bad ↔ apeb.bad)
                ∧ (  ¬ peb.bad
                   →   peb.fill = (apeb.echdr = empty ⊃ 0;(apeb.vidhdr = empty ⊃ EB_PAGE_SIZE;apeb.fill + 2 * EB_PAGE_SIZE))
                     ∧ abs-echdr(subarray(peb.data, 0, EB_PAGE_SIZE), apeb.echdr)
                     ∧ abs-vidhdr(subarray(peb.data, EB_PAGE_SIZE, EB_PAGE_SIZE), apeb.vidhdr)
                     ∧ subarray(peb.data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apeb.data);
          used for: ls;
          abs-echdr
          : ⊦   abs-echdr(buf, aehdr)
              ↔   (aehdr = empty → buf = emptypage) ∧ (aehdr.valid? → is-encoded(echdr(aehdr.ec), buf))
                ∧ (aehdr = garbage → is-garbage-ec(buf) ∧ buf ≠ emptypage);
          used for: ls;
          abs-vidhdr
          : ⊦   abs-vidhdr(buf, avhdr)
              ↔   (avhdr = empty → buf = emptypage)
                ∧ (avhdr.valid? → is-encoded(vidhdr(avhdr.vol, avhdr.leb, avhdr.sqn, avhdr.size, avhdr.checksum), buf))
                ∧ (avhdr = garbage → is-garbage-vid(buf) ∧ buf ≠ emptypage);
          used for: ls;
          initial-apebs-size :  ⊦ # initial-apebs(pebs) = # pebs;
          used for: s, ls;
          initial-apebs-at :  ⊦ n < # pebs → initial-apebs(pebs)[n] = mkpeb(empty, empty, emptyleb, 0, pebs[n].bad);
          used for: s, ls;

   

   
end enrich