[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 abs-node
enrich
   encoding-node-base

with
   

   
   
   
   predicates  abs-node : buffer × elem;
               abs-padding : buffer;
               abs-failed : buffer;
   
   
   
   

   

   axioms abs-failed
          : ⊦   abs-failed(buf)
              ↔   # buf ≥ NODE_HEADER_SIZE ∧ is-aligned(# buf, NODE_HEADER_SIZE)
                ∧ (∃ buf0, buf1. 
                       buf = buf0 + buf1 ∧ # buf0 = NODE_HEADER_SIZE
                     ∧ (is-garbage-header(buf0) ∨ (∃ ndhd. is-encoded(ndhd, buf0) ∧ # buf1 ≤ align↑(ndhd.size, 2 * NODE_HEADER_SIZE))));
          used for: ls;
          abs-node
          : ⊦   abs-node(buf, nd)
              ↔ (∃ buf0, buf1. 
                     buf = buf0 + buf1 + validtrailer ∧ is-encoded(nodeheader(node-size-headerless(nd), false), buf0)
                   ∧ is-encoded(nd, subarray(buf1, 0, node-size-headerless(nd))) ∧ # buf1 = nd.alignedsize);
          used for: ls;
          abs-padding
          : ⊦   abs-padding(buf)
              ↔ (∃ buf0, buf1. 
                   buf = buf0 + buf1 + validtrailer ∧ is-encoded(nodeheader(# buf1, true), buf0) ∧ is-aligned(# buf1, 2 * NODE_HEADER_SIZE));
          used for: ls;

   

   
end enrich