Specification refinement

[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 queue , 
       queue-impl with
   functions 
      tolist : ring_buffer × nat → queue;
   predicates 
      abs : ring_buffer × queue;
   
   axioms 
      abs :  ⊦ abs(buf, x) ↔ buf .len = n→i(# x) ∧ x = tolist(buf, i→n(buf .len));
      used for : s, ls;
       
      tolist-base :  ⊦ tolist(buf, 0) = [];
      used for : s, ls;
       
      tolist-rec
      : ⊦ 
          (i→n(buf .first) + n) % i→n(buf .size) < # buf .data
        → tolist(buf, n + 1) = push(tolist(buf, n), (buf .data)[(i→n(buf .first) + n) % i→n(buf .size)]);
      used for : s, ls;
       
end enrich