DFS progress

TODO

 
 
+- xwhile needs to call tag_pre_post in branches
+
 
 
 - hint spec based on type args

examples/BasicDemos/Demo_proof.v

 Set Implicit Arguments.
-(* LibInt LibWf *)
 Require Import CFLib.
 Require Import Demo_ml.
 Require Import Stdlib.
- Open Scope tag_scope.
+Open Scope tag_scope.
+
+
+
+(********************************************************************)
+(********************************************************************)
+
+(*----
+DEMO
+
+
+  (* TODO: fix hack *)
+
+  Definition Zsub := Zminus.
+
+  Infix "-" := Zsub : Int_scope.
+
+  Open Scope Int_scope.
+
+  Lemma Zsub_eq : Zsub = Zminus.
+  Proof using. auto. Qed.
+
+  Opaque Zsub.
+
+  Hint Rewrite Zsub_eq : rew_maths.
+
+  (* end hack *)
+
+  (* TODO: move *)
+  Hint Rewrite downto_def nat_upto_wf upto_def : rew_maths.
+
+
+  Ltac auto_star ::= subst; intuition eauto with maths.
+
+  Lemma while_decr_spec' : 
+    app while_decr [tt] \[] \[= 3].
+  Proof using.
+    xcf.
+    xapps. xapps. 
+    xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
+                           \* n ~~> k \* c ~~> (3-k)) (downto 0).
+      xgo*.
+      intros. xpull. intros. xgo*.
+      intros. xpull. intros. xgo*.
+      xgo*.
+    intros. xpull. intros. xgo*.
+  Qed.
+
+
+
+  Proof using.
+    xgo. 
+    xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
+                           \* n ~~> k \* c ~~> (3-k)) (downto 0).
+      xgo*.
+    xgo*.
+  Qed.
+
+
+
+
+  Lemma while_decr_spec : 
+    app while_decr [tt] \[] \[= 3].
+  Proof using.
+    xcf.
+    (* xlet. xapp1. xapp2. apply Spec. simpl. *)
+    xapp. 
+    xapp. 
+    xseq.
+    { xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
+                           \* n ~~> k \* c ~~> (3-k)) (downto 0).
+      { xsimpl*. math. }
+      { xtag_pre_post. intros b k. xpull ;=> Hk Hb. xapps. xrets. xauto*. math. }
+      { xtag_pre_post. intros k. xpull ;=> Hk Hb. xapps. xapps. simpl. xsimpl. math. eauto. math. math. } 
+     }
+   xpull. => k Hk Hb. fold_bool. xclean. xapp. xsimpl. math.
+  Abort.
+
+
+
+----*)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+(********************************************************************)
+(********************************************************************)
+
+
+
 
 
 (*

examples/DFS/DFS.ml

 
-
-
-
-
 (*************************************************************************)
 (** Graph representation by adjacency lists *)
 
-module GraphAdj = struct
+module Graph = struct
 
-type 'a t = ((int*'a) list) array 
+type t = (int list) array 
 
-let nb_nodes (g:'a t) = 
+let nb_nodes (g:t) = 
   Array.length g
 
-let iter_edges_of (g:'a t) (i:int) (f:int->'a->unit) =
-  List.iter (fun (j,w) -> f j w) g.(i)
-
-let iter_edges_target_of (g:'a t) (i:int) (f:int->unit) =
-  List.iter (fun (j,_) -> f j) g.(i)
-
-let fold_edges_target_of (g:'a t) (i:int) (a:'b) (f:'b->int->'b) =
-  List.fold_left (fun acc (j,_) -> f acc j) a g.(i)
-
-let iter_nodes (g:'a t) (f:int->unit) =
-   for i = 0 to (nb_nodes g)-1 do
-      f i
-   done
-
-let fold_nodes (g:'a t) (a:'b) (f:'b->int->'b) =
-   let r = ref a in
-   for i = 0 to (nb_nodes g)-1 do
-      r := f !r i
-   done
+let iter_edges (f:int->unit) (g:t) (i:int) =
+  List.iter (fun j -> f j) g.(i)
 
 end
 
 
-
-type color = White | Gray | Black
-
-(*
-let reachable_recursive g a b =
-   let n = GraphAdj.nb_nodes g in
-   let c = Array.make n White in
-   visit a;
-   c.(b)
-*)
-
-let rec dfs_from g c i =
-   let rec visit i =
-      c.(i) <- Gray;
-      GraphAdj.iter_edges_target_of g i (fun j -> 
-         if c.(j) = White 
-            then visit j);
-      c.(i) <- Black;
-      in
-   visit i
-
-let dfs_main (g : unit GraphAdj.t) =
-   let n = GraphAdj.nb_nodes g in
-   let c = Array.make n White in
-   for i = 0 to n - 1 do
-     if c.(i) = White then
-       dfs_from g c i
-   done
-
-
-
-
-
-(*
-
-
 (*************************************************************************)
-(** GraphAdj representation by adjacency matrix --LATER *)
-
-module GraphMat = struct
-
-type 'a t = ('a array) array 
-
-let nb_nodes (g:'a t) = 
-  Array.length g
-
-let get_edge (g:'a t) i j =
-   g.(i).(j)
-
-let set_edge (g:'a t) i j w =
-   g.(i).(j) <- w
-
-let has_edge (g:bool t) i j =
-   get_edge g i j
-
-let add_edge (g:bool t) i j =
-   set_edge g i j true
-
-end
-
-
-(*************************************************************************)
-(** Reachability by recursive DFS, three-colored *)
+(** DFS Algorithm, Sedgewick's presentation *)
 
 type color = White | Gray | Black
 
-let reachable_recursive g a b =
-   let n = GraphAdj.nb_nodes g in
-   let c = Array.make n White in
-   let rec visit i =
-      c.(i) <- Gray;
-      GraphAdj.iter_edges_target_of g i (fun j -> 
-         if c.(j) = White 
-            then visit j);
-      c.(i) <- Black;
-      in
-   visit a;
-   c.(b)
-
-
-(*************************************************************************)
-(** Reachability by imperative DFS, two-colored *)
-
-let reachable_imperative g a b = 
-   let n = GraphAdj.nb_nodes g in
-   let c = Array.make n false in
-   let s = Stack.create() in
-   c.(a) <- true; 
-   Stack.push a s;
-   while not (Stack.is_empty s) do
-      let i = Stack.pop s in
-      GraphAdj.iter_edges_target_of g i (fun j -> 
-         if not c.(j) then begin 
-           c.(i) <- true; 
-           Stack.push i s;
-         end);
-   done;
-   c.(b)
-
-
-(*************************************************************************)
-(** Cycle detection by recursive DFS, three-colored *)
-
-(** Note: for simlicity, the current implementation does not exit 
-    abruptly when detecting a cycle. *)
+ let rec dfs_from g c i =
+    c.(i) <- Gray;
+    Graph.iter_edges (fun j -> 
+       if c.(j) = White 
+          then dfs_from g c j) g i;
+    c.(i) <- Black
 
-let cycle_detection g s e =
-   let n = GraphAdj.nb_nodes g in
+let dfs_main g r =
+   let n = Graph.nb_nodes g in
    let c = Array.make n White in
-   let r = ref false in
-   let rec visit i =
-      c.(i) <- Gray;
-      GraphAdj.iter_edges_target_of g i (fun j -> 
-         if c.(j) = White 
-            then visit j
-         else if c.(j) = Gray
-            then r := true);
-      c.(i) <- Black;
-      in
-   GraphAdj.iter_nodes g (fun i ->
-      if c.(i) = White then visit i);
-   !r
-
-
-(*************************************************************************)
-(** Topological sort, without cycle detection *)
-
-(* Note: it would be straightforward to add cycle detection. *)
-
-let topological_sort g s e =
-   let n = GraphAdj.nb_nodes g in
-   let neverseen = -1 in
-   let processed = -2 in
-   let c = Array.make n neverseen in
-   let k = ref (n-1) in
-   let rec visit i =
-      c.(i) <- processed;
-      GraphAdj.iter_edges_target_of g i (fun j -> 
-         if c.(j) = neverseen 
-            then visit j);
-      c.(i) <- !k;
-      decr k;
-      in
-   GraphAdj.iter_nodes g (fun i ->
-      if c.(i) = neverseen then visit i);
-   c
-
-
-(*************************************************************************)
-(** Connected components by recursive DFS, two-colored *)
-
-let connected_recursive g = 
-   let n = GraphAdj.nb_nodes g in
-   let neverseen = -1 in
-   let c = Array.make n neverseen in
-   let k = ref 0 in
-   let rec visit i =
-      c.(i) <- !k;
-      GraphAdj.iter_edges_target_of g i (fun j -> 
-         if c.(j) = neverseen
-            then visit j)
-      in
-   GraphAdj.iter_nodes g (fun i ->      
-      if c.(i) = neverseen then begin
-         visit i;
-         incr k
-      end);
-   c
-
-(*************************************************************************)
-(** Spanning forest by recursive DFS *)
-
-(** Note: the inductive type is defined in a funny way just to please Coq. *)
-
-type tree = Tree of int * tree list
-type forest = tree list
-
-let spanning_forest g = 
-   let n = GraphAdj.nb_nodes g in
-   let c = Array.make n false in
-   let rec build_tree i =
-      c.(i) <- true;
-      let ts = GraphAdj.fold_edges_target_of g i [] harvest in
-      Tree (i,ts) 
-   and harvest acc i = 
-      if c.(i) then acc else (build_tree i)::acc 
-   in
-   GraphAdj.fold_nodes g [] harvest
-
-
-(*************************************************************************)
-(** Connected components by imperative DFS *)
-
-let connected_imperative g =
-   let n = GraphAdj.nb_nodes g in
-   let neverseen = -1 in
-   let c = Array.make n neverseen in
-   let k = ref 0 in
-   let s = Stack.create() in
-   let find i =
-      c.(i) <- !k; 
-      Stack.push i s
-      in
-   GraphAdj.iter_nodes g (fun i ->
-      if c.(i) = neverseen then begin
-         find i;
-         while not (Stack.is_empty s) do
-            let i = Stack.pop s in
-            GraphAdj.iter_edges_target_of g i (fun j -> 
-               if c.(j) = neverseen 
-                  then find j)
-         done;
-         incr k;
-      end);
+   List.iter (fun i -> 
+     if c.(i) = White then
+       dfs_from g c i) r;
    c
-
-
-(*************************************************************************)
-(** Connected components by warshall-floyd *)
-
-(** Note: implemented by side-effects on the adjacency matrix *) 
-
-let connected_warshall_floyd g =
-   let n = GraphMat.nb_nodes g in
-   for k = 0 to n-1 do
-      for i = 0 to n-1 do
-         for j = 0 to n-1 do
-            if    GraphMat.has_edge g i k
-               && GraphMat.has_edge g k j
-               then GraphMat.add_edge g i j
-         done;
-      done;
-   done
-
-(* TODO:
-   for each node
-      if node not marked
-         nbcompo++
-         foreach neighbor
-            mark it
-         
-*)
-
-
-(*************************************************************************)
-(** Strongly connected components, Kosaraju's algorithm (2 DFS) *)
-
-(*************************************************************************)
-(** Strongly connected components, Tarjan's algorithm *)
-
-(*************************************************************************)
-(** Strongly connected components, path-based algorithm *)
-
-(*************************************************************************)
-(** Edge cut *)
-
-(*************************************************************************)
-(** Vertex cut *)
-
-(*************************************************************************)
-(** Eulerian path *)
-
-*)
\ No newline at end of file

examples/DFS/DFS_why3.mlw

+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 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 -> x' \in (blacks \u grays) 
+
+  lemma black_to_white_path_goes_thru_gray:
+    forall grays blacks. no_black_to_white blacks grays -> 
+      forall x l 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 {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
+
+
+end
+Generated by why3doc 0.86.1
\ No newline at end of file