[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
   linked-list, 
   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  r : ref;
              a : elem;
              b : elem;
              x : list;
              y : list;
              h : heap;
              hP : heap → bool;
              ce : cell;
   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) * hP))(h) ↔ (∃ x0, x1. x = x0 + x1 ∧ ((lls(r0, r1, x0) * lls(r1, null, x1) * hP))(h));
      used for: ls;
      ll-trav2-null-def :  ⊦ ((ll-trav(r0, null, r2, x) * hP))(h) ↔ r2 = r0 ∧ ((lls(r0, null, x) * hP))(h);
      used for: ls;
      ll-trav2-nonnull-def
      : ⊦   r1 ≠ null
          → (((ll-trav(r0, r1, r2, x) * hP))(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ((lls(r0, r1, x0) * r1 => a × r2 * lls(r2, null, x1) * hP))(h)));
      used for: ls;

   
end enrich