[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-list
enrich
   awbuf-inv
, 
   abs-node, 
   list-prefixn
, 
   laddress-list

with
   

   
   
   functions  . .flashsize : list → nat;
   predicates  abs-nodes : buffer × list × laddress-list × bool;
               abs-nodes : buffer × nat × list × laddress-list × bool;
   
   variables  weak : bool;
   
   

   

   axioms abs-nodes :  ⊦ abs-nodes(buf, x, lax, weak) ↔ abs-nodes(buf, 0, x, lax, weak);
          used for: ls;
          abs-nodes-base
          : ⊦   abs-nodes(buf, m, [], lax, weak)
              ↔   # buf = 0 ∧ lax = [] ∨ (∃ buf0, buf1. buf = buf0 + buf1 ∧ abs-padding(buf0) ∧ abs-nodes(buf1, m + # buf0, [], lax, weak))
                ∨ weak ∧ abs-failed(buf) ∧ lax = [];
          abs-nodes-rec
          : ⊦   abs-nodes(buf, m, a ' + x, lax, weak)
              ↔ (∃ buf0, buf1. 
                     buf = buf0 + buf1
                   ∧ (  abs-padding(buf0) ∧ abs-nodes(buf1, m + # buf0, a ' + x, lax, weak)
                      ∨   lax ≠ [] ∧ lax.head.off = m ∧ lax.head.size = # buf0 ∧ abs-node(buf0, a)
                        ∧ abs-nodes(buf1, m + # buf0, x, lax.tail, weak)));
          size-base :  ⊦ [].flashsize = 0;
          used for: s, ls;
          size-rec :  ⊦ (a ' + x).flashsize = a.flashsize + x.flashsize;
          used for: s, ls;

   

   
end enrich