[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-fixed-size-nonempty
enrich
   encoding-fixed-size
, 
   eraseblock, 
   debug
with
   

   
   
   
   predicates  is-encoded-nonempty : elem × buffer;
               is-garbage-nonempty : buffer;
   procedures encode_nonempty# elem × nat : buffer : error  nondeterministic;
              decode_nonempty# nat × buffer : elem : error  nondeterministic;
   
   
   

   

   axioms is-encoded-nonempty :  ⊦ is-encoded-nonempty(a, buf) ↔ is-encoded(a, buf) ∧ ¬ isempty(buf);
          used for: ls;
          is-garbage-nonempty :  ⊦ is-garbage-nonempty(buf) ↔ (∀ a. ¬ is-encoded-nonempty(a, buf));
          used for: ls;

   

   declarations encode
                : encode_nonempty#(a, n; buf; err)
                  {let m = ?
                   in {encode#(a, n; buf, m; err); 
                       if err = ESUCCESS ∧ isempty(buf, n, m) then {debug#("encoding_nonempty: encoding is empty"); err := EINVAL}}
                  }
                ;
                decode
                : decode_nonempty#(n, buf; a; err)
                  {if isempty(buf, n, ENCODED_ELEM_SIZE) then err := EINVAL else let m = ? in decode#(n, buf; a, m; err)}
                ;
end enrich