why3doc index index



Acyclicity test in Graph

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

The algorithm makes simple depth-first-search in the graph, looking for a loop-back to a gray node.
Fully automatic proof.


module DagTest
  use import int.Int
  use import int.MinMax
  use import list.List
  use import list.Length
  use import list.Append
  use import list.Mem as L
  use import list.NumOcc
  use import list.Elements as E
  use import list.HdTlNoOpt
  use import init_graph.GraphSetSucc
  use import map.Map
  use import ref.Ref
  use import ref.Refint
 
predicate lmem (x: 'a) (s: list 'a) = L.mem x s

Ranks and Lists


(* simple lists *)

predicate simplelist (l: list 'a) = forall x. num_occ x l <= 1

Sets


lemma inter_assoc:
  forall s1 s2: set 'a. inter s1 s2 == inter s2 s1

lemma inter_add:
  forall s1 s2: set 'a, x: 'a. not mem x s2 -> inter (add x s1) s2 == inter s1 s2

lemma inter_subset_inter:
  forall s1 s2 s3: set 'a. inter s1 s2 = empty -> subset s3 s2 -> inter s1 s3 = empty

lemma subset_add:
  forall x: 'a, s s': set 'a. subset s' (add x s) -> mem x s' \/ subset s' s

Predicates definitions


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

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

predicate circle (x: vertex) (l: list vertex) =
  l <> Nil /\ simplelist l /\ path x l x 

predicate black_circle (x: vertex) (l: list vertex) (b: set vertex) =
  circle x l /\ subset (elements l) b

predicate reachable (x z: vertex) =
  exists l. path x l z
    
predicate access_to (s: set vertex) (y: vertex) =
  forall x. mem x s -> reachable x y

Specialized lemmas


use import list.Permut

lemma circle_rotate:
  forall x y l1 l2. circle x (Cons x (l1 ++ Cons y l2)) -> circle y (Cons y (l2 ++ Cons x l1))

let lemma circle_rotate_to (x y: vertex) (l: list vertex) 
  requires {circle x l}
  requires {lmem y l}
  ensures {exists l'. circle y l' /\ permut l l'}
= if y = x then () else
     assert {exists l1 l2. l = Cons x l1 ++ Cons y l2}; ()

dfs1


predicate wff_color (blacks grays: set vertex) = 
  no_black_to_white blacks grays /\ no_black_to_gray blacks grays /\ inter blacks grays = empty

use import list.Reverse

predicate gray_chain_edge (s: list vertex) (x: vertex) =
  s <> Nil -> edge (hd s) x /\ path (hd (reverse s)) (reverse s) x /\ simplelist s 

lemma simple_list_decomp:
  forall l1 l2: list 'a. simplelist (l1 ++ l2) -> simplelist l1 /\ simplelist l2

lemma simple_non_empty_path_decomp_general:
  forall x l z y. path x l z -> simplelist l -> lmem y l -> exists l'. path y l' z /\ simplelist l' /\ l' <> Nil
  
let rec dfs1 x blacks grays (ghost stack) =
requires {mem x vertices}
requires {grays == elements stack}
requires {gray_chain_edge stack x}
requires {not mem x (union blacks grays)}
(* invariants *)
requires {wff_color blacks grays}
requires {forall x l. not black_circle x l blacks}
returns {(r, b) -> r -> wff_color b grays}
returns {(r, b) -> r -> forall x l. not black_circle x l b}
returns {(r, _) -> not r -> exists x l. circle x l}
(* post-conditions *)
returns {(_, b) -> mem x b}
(* monotony *)
returns {(_, b) -> subset blacks b}

  let (r1, b1) =
  dfs' (successors x) blacks (add x grays) (Cons x stack) in
  assert {forall y l. black_circle y l (add x b1) -> lmem x l -> exists l'. black_circle x l' (add x b1)};    
  assert {forall l. black_circle x l (add x b1) -> exists y. edge y x /\ mem y (add x b1)}; 
  (r1, add x b1)

dfs'


with dfs' roots blacks grays (ghost stack) =
requires {subset roots vertices}
requires {grays == elements stack}
requires {forall x. mem x roots -> gray_chain_edge stack x}
(* invariants *)
requires {wff_color blacks grays}
requires {forall x l. not black_circle x l blacks}
returns {(r, b) -> r -> wff_color b grays}
returns {(r, b) -> r -> forall x l. not black_circle x l b}
returns {(r, _) -> r = false -> exists x l. circle x l}
(* post-conditions *)
returns {(r, b) -> r -> subset roots b}
(* monotony *)
returns {(_, b) -> subset blacks b}

  if is_empty roots then (true, blacks)
  else
     let y = choose roots in
     let roots' = remove y roots in
     if mem y grays then (false, blacks)
     else
       let (r3, b3) = 
         if mem y blacks then (true, blacks)
	 else dfs1 y blacks grays stack in
       if r3 then dfs' roots' b3 grays stack
       else (false, b3)
         
  
let dag_main () = 
returns {(r, _) -> r = not exists x l. circle x l /\ subset (elements l) vertices}
  dfs' vertices empty empty Nil

[all proof is here (zip file)]


end

Generated by why3doc 0.87.0