Depth First Search (nbtw assumption)

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

• vertices : this constant is the set of graph vertices
• successor : this function gives for each vertex the set of vertices directly joinable from it

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, except Coq used to prove inductive post-condition of dfs_main via lemma no_black_to_white_nopath

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
  use import init_graph.GraphSetSuccPath

  predicate white_vertex (x: vertex) (v: set vertex) =
    not (mem x v)
 
  predicate white_monotony (v1 v2: set vertex) =
    forall x: vertex. white_vertex x v2 -> white_vertex x v1

  predicate nodeflip (x: vertex) (v1 v2: set vertex) =
    white_vertex x v1 /\ not (white_vertex x v2)

  predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) =
    path x l z /\ (forall y. L.mem y l -> white_vertex y v) /\ white_vertex z v

  lemma whitepath_mem_decomp:  
    forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v

  lemma whitepath_mem_decomp_right:
    forall x l z y v. whitepath x l z v -> L.mem y (l ++ (Cons z Nil)) -> exists l': list vertex. whitepath y l' z v
    
  predicate nodeflip_whitepath (roots v1 v2: set vertex) =
    forall z. nodeflip z v1 v2 -> exists x l. mem x roots /\ whitepath x l z v1 

  predicate whitepath_nodeflip (roots v1 v2: set vertex) =
    forall x l z. mem x roots -> whitepath x l z v1 -> nodeflip z v1 v2

  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 grays blacks. no_black_to_white blacks grays -> 
      forall x l "induction" z. path x l z -> mem x blacks -> not mem z (union blacks grays) ->
        exists y. L.mem y l /\ mem y grays

let rec dfs (roots grays blacks: set vertex): set vertex 
  variant {(cardinal vertices - cardinal grays), (cardinal roots)} =
  requires {subset roots vertices}  
  requires {subset grays vertices}  
  requires {no_black_to_white blacks grays}
  ensures {subset blacks result}  
  ensures {no_black_to_white result grays}
  ensures {forall x. mem x roots -> not mem x grays -> mem x result} 
  ensures {access (union blacks roots) result}

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

let dfs_main (roots: set vertex) : set vertex =
   requires {subset roots vertices}
   ensures {whitepath_nodeflip roots empty result}
   ensures {nodeflip_whitepath roots empty result}
   dfs roots empty empty

end