[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 valid-peb
enrich
   ubi-io-inv

with
   

   
   
   
   predicates  valid-peb : volid × nat × apeb;
               valid-peb : apeb;
   
   
   
   

   

   axioms valid-peb2
          : ⊦   valid-peb(v, m, apeb)
              ↔   ¬ apeb.bad ∧ apeb.echdr.valid?
                ∧ (∃ m0, m1, m2. apeb.vidhdr = avidhdr(v, m, m0, m1, m2) ∧ (m1 ≠ 0 → m1 ≤ datasize(apeb.data) ∧ m2 = checksum(apeb.data, m1)));
          used for: ls;
          comment: holds if the PEB is not marked as bad, contains a valid VID-header and if the PEB is a copy the data's checksum is valid;
          valid-peb0 :  ⊦ valid-peb(apeb) ↔ (∃ v, m. valid-peb(v, m, apeb));
          used for: ls;

   

   
end enrich