[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 linked-list-seg
enrich
   cell-heap, 
   list-last

with
   

   
   
   functions  lls : ref × ref × list → heap → bool;
              ll-trav : ref × ref × list → heap → bool;
              ll-trav : ref × ref × ref × list → heap → bool;
   
   
   variables  r2 : ref;
   
   

   

   axioms lls-base :  ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ );
          used for: s, ls;
          lls-rec :  ⊦ lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x));
          used for: s, ls;
          ll-trav1-def :  ⊦ ((ll-trav(r0, r1, x) * P))(H) ↔ (∃ x0, x1. x = x0 + x1 ∧ ((lls(r0, r1, x0) * lls(r1, null, x1) * P))(H));
          used for: ls;
          ll-trav2-null-def :  ⊦ ((ll-trav(r0, null, r2, x) * P))(H) ↔ r2 = r0 ∧ ((lls(r0, null, x) * P))(H);
          used for: ls;
          ll-trav2-nonnull-def
          : ⊦   r1 ≠ null
              → (  ((ll-trav(r0, r1, r2, x) * P))(H)
                 ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ((lls(r0, r1, x0) * r1 => a × r2 * lls(r2, null, x1) * P))(H)));
          used for: ls;

   

   
end enrich