[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 INV
enrich graph with
comment: specification of the main invariants of the algorithm BFS, 
and proofs that they are invariant for the main steps of the
body: ADD and moving N to C.;
   predicates 
      INV : set × set × set × nat × elem;
      INVR : set × set × set × nat × nat × elem × elem;
   variables 
      source, dest : elem; 
      V, C, N : set; 
      v, w : elem; 
      done : bool; 
   
   axioms 
      INVR-def
      : ⊦ 
          INVR(C, N, V, n, n0, source, dest)
        ↔ ¬ ¬ (  reach(source, dest, n0) ∧ ¬ reach<(source, dest, n0) ∧ n ≤ n0
               ∧ ((∃ a. a ∈ C ∧ reachS(a, {dest} , n0 - n)) ∨ n < n0 ∧ (∃ b. b ∈ N ∧ reachS(b, {dest} , n0 - n - 1))));
      comment: double negation says: always unfold INV.;
      used for : ls;
       
      INV-def
      : ⊦ 
          INV(C, N, V, n, source)
        ↔ ¬ ¬ (  (∀ b. b ∈ V ↔ reach<(source, b, n + 1) ∨ (∃ a. b ∈ succ(a) ∧ reachS(source, {a} , n) ∧ ¬ a ∈ C)) ∧ reachS(source, C, n)
               ∧ reachS(source, N, n + 1) ∧ (∀ b. reachS(source, {b} , n + 1) → b ∈ N ∨ (∃ a. a ∈ C ∧ b ∈ succ(a) ∧ ¬ b ∈ V)));
      comment: double negation says: always unfold INV.;
      used for : ls;
       
end enrich