[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 dlinked-list
enrich
   node, 
   separation, 
   list
with
   functions 
       dll : Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool;
       dll : Ref[Node[A]] × Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool;
   
   variables 
       r : Ref[Node[A]];
       x : List[A];
       y : List[A];
       z : List[A];
       a : A;
       b : A;
       c : A;
       h : Heap[Node[A]];
       hP : Heap[Node[A]] → Bool;
       nd : Node[A];
   
   
   axioms 
      dll: dll(r, x) = dll(r, null, x);
      used for: s, ls;
      
      dll-base: dll(r, r0, []) = (emp ∧ ⌜r = null⌝ );
      used for: s, ls;
      
      dll-rec: dll(r, r0, a ' + x) = _∃(λ r1. r => mknode(r0, a, r1) * dll(r1, r, x));
      used for: s, ls;
   
   
end enrich