[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 encoding-lpt
enrich
   encoding-lprops
, 
   lp-array
, 
   eraseblock

with
   

   
   
   functions  lptsize : nat × nat → nat;
              lptlebs : nat × nat → nat;
   predicates  is-encoded : lp-array × buffer × nat;
               is-encoded : lp-array × buffer;
   
   variables  mainareasize : nat;
   
   

   

   axioms is-encoded
          : ⊦   is-encoded(lpt, buf, n)
              ↔   # buf = lptsize(# lpt, LEB_SIZE)
                ∧ (∀ m. m < # lpt ∧ m < n → is-encoded(lpt[m], subarray(buf, m * ENCODED_LPROPS_SIZE, ENCODED_LPROPS_SIZE)));
          is-encoded-full :  ⊦ is-encoded(lpt, buf) ↔ is-encoded(lpt, buf, # lpt);
          lpt-size :  ⊦ lptsize(mainareasize, n) = align↑(mainareasize * ENCODED_LPROPS_SIZE, n);
          used for: ls;
          lpt-lebs :  ⊦ lptlebs(mainareasize, n) = lptsize(mainareasize, n) / n;
          used for: ls;

   

   
end enrich