Wiki Agenda Contact Version française

Topological sorting


Authors: François Bobot

Topics: Graph Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



Topological sorting

Author: Fran├žois Bobot (CEA)

theory Graph

  use export int.Int
  use set.Fset as S
  use map.Map as M

  (* the graph is defined by a set of vertices and a set of edges *)
  type vertex
  type graph

  function vertices graph: S.set vertex

  function edges graph: S.set (vertex , vertex)

  axiom edges_use_vertices:
  forall g:graph. forall x y:vertex.
    S.mem (x,y) (edges g) -> (S.mem x (vertices g) /\ S.mem y (vertices g))

direct predecessors

  function preds graph vertex: S.set vertex

  axiom preds_def:  forall g:graph. forall v:vertex. forall u:vertex.
   S.mem (u,v) (edges g) <-> S.mem u (preds g v)

direct successors

  function succs graph vertex: S.set vertex
  axiom succs_def:  forall g:graph. forall v:vertex. forall u:vertex.
   S.mem (u,v) (edges g) <-> S.mem v (succs g u)

  type msort = M.map vertex int

  predicate sort (g: graph) (m:msort) =
    forall v:vertex. forall u:vertex.
    S.mem (u,v) (edges g) ->
    (M.get m u) < (M.get m v)

end

static topological sorting by depth-first search

module Static

  use import ref.Ref
  use import Graph
  use set.Fset as S
  use map.Map as M
  use map.Const

  function defined_sort (m:msort) : S.set vertex
  axiom defined_sort_def:
   forall m:msort. forall v: vertex[S.mem v (defined_sort m)].
    S.mem v (defined_sort m) <-> 0 <= M.get m v

  predicate partial_sort (g: graph) (m:msort) =
    forall v:vertex. forall u:vertex.
    S.mem (u,v) (edges g) -> 0 <= (M.get m v)
     -> 0 <= (M.get m u) < (M.get m v)

  type marked = (S.set vertex)

  exception Cycle_found

  predicate inv (g:graph) (m:msort) (next:int) =
    S.subset (defined_sort m) (vertices g) &&
    0 <= next &&
    partial_sort g m &&
    forall v:vertex. S.mem v (defined_sort m) -> M.get m v < next

  let rec dfs (g:graph) (v:vertex)
              (seen:marked) (values:ref msort) (next: ref int) : unit
    requires { inv g !values !next }
    requires { S.mem v (vertices g) }
    requires { S.subset seen (vertices g) }
    variant { S.cardinal (vertices g) - S.cardinal seen }
    ensures { S.subset (old (defined_sort !values)) (defined_sort !values) }
    ensures { 0 <= M.get !values v <= !next}
    ensures { inv g !values !next }
    ensures { forall x:vertex. S.mem x seen -> M.get (old !values) x = M.get !values x }
    raises  { Cycle_found -> true }
   =
  'Init:
   if S.mem v seen then raise Cycle_found;
   if not (0 <= M.get !values v) then
  'Init_loop:
    begin
     let p = ref (preds g v) in
     let seen = S.add v seen in
     while not (S.is_empty !p) do
      invariant { inv g !values !next }
      invariant { S.subset (S.diff (preds g v) !p) (defined_sort !values) }
      invariant { S.subset (at (defined_sort !values) 'Init) (defined_sort !values) }
      invariant { S.subset !p (preds g v) }
      invariant { forall x:vertex. S.mem x seen -> M.get (at !values 'Init_loop) x = M.get !values x }
      variant {S.cardinal !p}
      let u = S.choose !p in
      dfs g u seen values next;
      p := S.remove u !p
      done;
    end;
    values := M.set !values v !next;
    next := !next + 1

    let topo_order (g:graph): msort
      raises  { Cycle_found -> true }
      ensures { sort g result }
      =
    'Init:
      let next = ref 0 in
      let values = ref (Const.const (-1)) in
      let p = ref (vertices g) in
      while not (S.is_empty !p) do
        invariant { inv g !values !next }
        invariant { S.subset !p (vertices g) }
        invariant { S.subset (S.diff (vertices g) !p) (defined_sort !values) }
        invariant { S.subset (at (defined_sort !values) 'Init) (defined_sort !values) }
        variant {S.cardinal !p}
        let u = S.choose !p in
        dfs g u (S.empty) values next;
        p := S.remove u !p
     done;
     !values

end

module Online_graph
  use export Graph

  function add_edge graph vertex vertex: graph
  axiom add_edge_def_preds:
    forall g:graph. forall u v:vertex.
      forall x.
        preds (add_edge g u v) x =
          if x = v then S.add u (preds g v) else preds g x

  axiom add_edge_def_succs:
    forall g:graph. forall u v:vertex.
      forall x.
        succs (add_edge g u v) x =
          if x = u then S.add v (succs g u) else succs g x

end

A New Approach to Incremental Topological Ordering Michael A. Bender, Jeremy T. Fineman, Seth Gilbert

module Online_Basic

  use import ref.Ref
  use import Online_graph
  use set.Fset as S
  use map.Map as M
  use map.Const

  type marked = (S.set vertex)

  exception Cycle_found

  type t = {
    mutable graph : graph;
    mutable values: msort;
 }

 predicate inv (g:t) = sort g.graph g.values

  let create (g:graph): t
     requires { forall x: vertex. S.is_empty (preds g x) }
     ensures  { result.graph = g }
     ensures  { inv result }
   =
    {graph = g; values = Const.const 0}

  let rec dfs (g:t) (v:vertex)
              (seen:marked) (min_depth:int) : unit
    requires { inv g }
    requires { S.mem v (vertices g.graph) }
    requires { S.subset seen (vertices g.graph) }
    raises  { Cycle_found -> true }
    variant { S.cardinal (vertices g.graph) - S.cardinal seen }
    ensures { min_depth <= M.get g.values v}
    ensures { inv g }
    ensures { forall x:vertex. S.mem x seen -> M.get (old g.values) x = M.get g.values x }
    ensures { forall x:vertex. M.get (old g.values) x <= M.get g.values x }
   =
  'Init:
   if S.mem v seen then raise Cycle_found;
   if M.get g.values v < min_depth then
  'Init_loop:
    begin
     let p = ref (succs g.graph v) in
     let seen = S.add v seen in
     while not (S.is_empty !p) do
      invariant { inv g }
      invariant { forall s:vertex. S.mem s (succs g.graph v) -> not (S.mem s !p) -> min_depth < M.get g.values s }
      invariant { S.subset !p (succs g.graph v) }
      invariant { forall x:vertex. S.mem x seen -> M.get (at g.values 'Init_loop) x = M.get g.values x }
      invariant { forall x:vertex. M.get (at g.values 'Init_loop) x <= M.get g.values x }
      variant {S.cardinal !p}
      let u = S.choose !p in
      dfs g u seen (min_depth + 1);
      p := S.remove u !p
      done;
    end;
    g.values <- M.set g.values v min_depth

  let add_edge (g:t) (x:vertex) (y:vertex): unit
     requires { inv g }
     requires { S.mem x (vertices g.graph) }
     requires { S.mem y (vertices g.graph) }
     ensures  { inv g }
     ensures  { g.graph = old (add_edge g.graph x y) }
     raises   { Cycle_found -> true } =
      dfs g y (S.singleton x) (M.get g.values x + 1);
      g.graph <- add_edge g.graph x y;

end

download ZIP archive

Why3 Proof Results for Project "topological_sorting"

Theory "topological_sorting.Static": fully verified in 2.53 s

ObligationsCVC4 (1.4)
VC for dfs---
split_goal_wp
  1. loop invariant init0.04
2. loop invariant init0.06
3. loop invariant init0.04
4. loop invariant init0.04
5. variant decrease0.05
6. precondition0.04
7. precondition0.17
8. precondition0.03
9. loop invariant preservation0.02
10. loop invariant preservation0.15
11. loop invariant preservation0.02
12. loop invariant preservation0.05
13. loop invariant preservation0.06
14. loop variant decrease0.06
15. postcondition0.08
16. postcondition0.05
17. postcondition---
inline_goal
  1. postcondition---
split_goal_wp
  1. VC for dfs0.11
2. VC for dfs0.02
3. VC for dfs---
inline_goal
  1. VC for dfs0.18
4. VC for dfs0.02
18. postcondition0.04
19. postcondition0.01
20. postcondition0.02
21. postcondition0.01
VC for topo_order---
split_goal_wp
  1. loop invariant init---
inline_goal
  1. loop invariant init---
split_goal_wp
  1. VC for topo_order0.07
2. VC for topo_order0.03
3. VC for topo_order0.06
4. VC for topo_order0.06
2. loop invariant init0.05
3. loop invariant init0.06
4. loop invariant init0.05
5. precondition0.05
6. precondition0.08
7. precondition0.08
8. loop invariant preservation0.05
9. loop invariant preservation0.10
10. loop invariant preservation0.16
11. loop invariant preservation0.08
12. loop variant decrease0.08
13. postcondition0.10

Theory "topological_sorting.Online_Basic": fully verified in 1.93 s

ObligationsCVC4 (1.4)
VC for create---
split_goal_wp
  1. postcondition0.06
VC for dfs---
split_goal_wp
  1. loop invariant init0.04
2. loop invariant init0.03
3. loop invariant init0.06
4. loop invariant init0.03
5. variant decrease0.05
6. precondition0.04
7. precondition0.15
8. precondition0.03
9. loop invariant preservation0.02
10. loop invariant preservation0.06
11. loop invariant preservation0.07
12. loop invariant preservation0.04
13. loop invariant preservation0.04
14. loop variant decrease0.06
15. postcondition0.02
16. postcondition0.78
17. postcondition0.04
18. postcondition0.02
19. postcondition0.01
20. postcondition0.01
21. postcondition0.01
VC for add_edge---
split_goal_wp
  1. precondition0.03
2. precondition0.03
3. precondition0.09
4. postcondition0.09
5. postcondition0.02