why3doc index index

Depth First Search (nbtw assumption)

The graph is represented by a pair (vertices, successor)

The algorithm is standard with gray/black sets of nodes. (white set is the union of their complements)
The proof assumes to start with non black-to-white colouring.
All proofs automatic.

Program logic with reachable inductive predicate, and access predicate.

module Dfs_nbtw
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Mem as L
  use import list.Elements as E
  use import init_graph.GraphSetSucc

  inductive reachable vertex vertex =
  | Reachable_empty:
      forall x: vertex. reachable x x
  | Reachable_cons:
      forall x y z: vertex.
      edge x y -> reachable y z -> reachable x z

(*  predicate reachable (x z: vertex) =
    exists l. path x l z  *)

  lemma reachable_succ:
    forall x x'. edge x x' -> reachable x x'

  lemma reachable_trans:
    forall x y z. reachable x y -> reachable y z -> reachable x z

  predicate access (roots b: set vertex) = forall z. mem z b -> exists x. mem x roots /\ reachable x z

  lemma access_monotony_l:
    forall roots roots' b. subset roots roots' -> access roots b -> access roots' b

  lemma access_monotony_r:
    forall roots b b'. subset b b' -> access roots b' -> access roots b

  lemma access_trans:
    forall roots b b'. access roots b' -> access b' b -> access roots b

  predicate no_black_to_white (blacks grays: set vertex) =
    forall x x'. edge x x' -> mem x blacks -> mem x' (union blacks grays) 

  lemma black_to_white_path_goes_thru_gray:
    forall g b. no_black_to_white b g -> 
      forall x z. reachable x z -> mem x b -> not mem z (union b g) ->
        exists y. reachable x y /\ mem y g 


let rec dfs r g b 
  variant {(cardinal vertices - cardinal g), (cardinal r)} =
  requires {subset r vertices}  
  requires {subset g vertices}  
  requires {no_black_to_white b g}
  ensures {subset b result}  
  ensures {no_black_to_white result g}
  ensures {forall x. mem x r -> not mem x g -> mem x result} 
  ensures {access (union b r) result}

  if is_empty r then b else
  let x = choose r in
  let r' = remove x r in
  if mem x (union g b) then dfs r' g b else 
  let b' = dfs (successors x) (add x g) b in
  assert{ access (add x b) b'};
  dfs r' g (add x b')

let dfs_main roots =
   requires {subset roots vertices}
   ensures {forall s. access roots s <-> subset s result}
   dfs roots empty empty

Thus the result of dfs_main is exactly the set of nodes reachable from roots



Generated by why3doc 0.88.3