[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 cyclic
enrich path-reachable
 , 
       nat-pot
 with
   
   predicates 
      cyclic : Ref × heap;
      legal : heap; comment: heap contains no dangling pointers;
   
   axioms 
      legal-def :  ⊦ legal(H) ↔ (∀ r. r ∈ H ∧ H[r] .nxt ≠ null → H[r] .nxt ∈ H);
      cyclic-def :  ⊦ cyclic(r, H) ↔ (∃ m, n, r0. m < n ∧ reachable-n(H, m, r, r0) ∧ reachable-n(H, n, r, r0));
   
end enrich