[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-aligned
enrich
   encoding-elem-alignment
, 
   encoding, 
   eraseblock
with
   

   
   
   functions  size-aligned : elem × nat → nat;
   predicates  is-encoded-aligned : elem × buffer;
   procedures encode_aligned# elem × nat × nat : buffer × nat : error  nondeterministic;
              decode_aligned# nat × buffer × nat : elem × nat : error  nondeterministic;
   
   
   

   

   axioms size-aligned :  ⊦ size-aligned(a, m) = align↑(encoding-size(a), m);
          is-encoded-aligned
          : ⊦   is-encoded-aligned(a, buf)
              ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ is-encoded(a, buf0) ∧ # buf = size-aligned(a, ENCODED_ELEM_ALIGNMENT));

   

   declarations encode : encode_aligned#(a, n, m; buf, n0; err){encode#(a, n; buf, n0; err); if err = ESUCCESS then n0 := align↑(n0, m)};
                decode
                : decode_aligned#(n, buf, m; a, n0; err)
                  {decode#(n, buf; a, n0; err); if err = ESUCCESS then {n0 := align↑(n0, m); if ¬ n + n0 ≤ # buf then err := EINVAL}}
                ;
end enrich