Specification encoding-page-size-nonempty

[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,

enrich
   encoding-fixed-size-nonempty

with
   

   
   
   
   predicates  is-encoded-pagesize : elem × buffer;
               is-garbage-pagesize : buffer;
   procedures encode_pagesize# nat × elem : buffer : error  nondeterministic;
              decode_pagesize# nat × buffer : elem : error  nondeterministic;
   
   
   

   

   axioms is-encoded-pagesize
          : ⊦   is-encoded-pagesize(a, buf)
              ↔   # buf = EB_PAGE_SIZE ∧ ENCODED_ELEM_SIZE ≤ EB_PAGE_SIZE ∧ is-encoded-nonempty(a, subarray(buf, 0, ENCODED_ELEM_SIZE))
                ∧ ¬ isempty(buf);
          used for: ls;
          is-garbage-pagesize :  ⊦ is-garbage-pagesize(buf) ↔ (∀ a. ¬ is-encoded-pagesize(a, buf));
          used for: ls;

   

   declarations encode : encode_pagesize#(n, a; buf; err){if ENCODED_ELEM_SIZE ≤ n then encode_nonempty#(a, 0; buf; err) else err := EINVAL};
                decode : decode_pagesize#(n, buf; a; err){if ENCODED_ELEM_SIZE ≤ n then decode_nonempty#(0, buf; a; err) else err := EINVAL};
end enrich