Specification path-reachable

[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
   store, 
   genlincell, 
   list-set
with
   comment: definition of paths and reachability from a root node for linear pointer structures.;
   predicates 
       path : list(Ref) × store(Ref, cell);
       reachable : Ref × Ref × store(Ref, cell);
       reachable* : store(Ref, cell) × Ref × Ref;
       reachable-n : store(Ref, cell) × nat × Ref × Ref;
       reachable-1 : store(Ref, cell) × Ref × Ref;
   
   variables 
       h : store(Ref, cell);
       x : list(Ref);
       y : list(Ref);
       r : Ref;
       n : nat;
       m : nat;
       ce : cell;
   
   
   axioms 
      reachable-1-def: reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0;
      
      reachable-star-def: reachable*(h, r, r0) ↔ (∃ n. reachable-n(h, n, r, r0));
      
      reachable-n-base: reachable-n(h, 0, r, r0) ↔ r = r0;
      
      reachable-n-rec: reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n, r1, r0));
      
      path-empty: ¬ path([], h);
      used for: s, ls;
      
      path-one: path(r ', h) ↔ r ∈ h ∧ r ≠ null;
      used for: s, ls;
      
      path-two: path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0;
      used for: s, ls;
      
      path-cons: path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h);
      used for: s, ls;
      
      reachable-def: reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0);
   
   
end enrich