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))

  function preds graph vertex: S.set vertex

direct predecessors

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

  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)

direct successors

  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

module Static

static topological sorting by depth-first search

  use ref.Ref
  use Graph
  use set.Fset as Fset

  clone impset.Impset as S with type elt = vertex
  clone appset.Appset as SA with type elt = vertex
  clone impmap.ImpmapNoDom with type key = vertex

  val ghost function defined_sort (m: t int): Fset.set vertex
    ensures { forall v: vertex [Fset.mem v result].
              Fset.mem v result <-> 0 <= m[v] }

  val get_preds (g: graph) (v: vertex): S.t
    ensures { result.S.contents = preds g v }

  val get_vertices (g: graph): S.t
    ensures { result.S.contents = vertices g }

  predicate partial_sort (g: graph) (m: t int) =
    forall v:vertex. forall u:vertex.
    Fset.mem (u,v) (edges g) -> 0 <= m[v] -> 0 <= m[u] < m[v]

  exception Cycle_found

  predicate inv (g: graph) (m: t int) (next: int) =
    Fset.subset (defined_sort m) (vertices g) &&
    0 <= next &&
    partial_sort g m &&
    forall v:vertex. Fset.mem v (defined_sort m) -> m[v] < next

  let rec dfs (g: graph) (v: vertex) (seen: SA.t) (values: t int) (next: ref int): unit
    requires { inv g values !next }
    requires { Fset.mem v (vertices g) }
    requires { Fset.subset seen.SA.contents (vertices g) }
    variant { Fset.cardinal (vertices g) - SA.cardinal seen }
    ensures { Fset.subset (defined_sort (old values)) (defined_sort values) }
    ensures { 0 <= values[v] <= !next}
    ensures { inv g values !next }
    ensures { forall x:vertex. SA.mem x seen -> old values[x] = values[x] }
    raises  { Cycle_found -> true }
  =
    if SA.mem v seen then raise Cycle_found;
    if values[v] < 0 then begin
      let p = get_preds g v in
      let seen = SA.add v seen in
      while not (S.is_empty p) do
        invariant { inv g values !next }
        invariant { Fset.subset (Fset.diff (preds g v) p.S.contents) (defined_sort values) }
        invariant { Fset.subset (defined_sort (old values)) (defined_sort values) }
        invariant { Fset.subset p.S.contents (preds g v) }
        invariant { forall x:vertex. SA.mem x seen -> values[x] = old values[x] }
        variant { S.cardinal p }
        let u = S.choose_and_remove p in
        dfs g u seen values next
      done;
      values[v] <- !next;
      next := !next + 1
    end

  let topo_order (g:graph): t int
    raises  { Cycle_found -> true }
    ensures { sort g result.contents }
  =
    let next = ref 0 in
    let values = create (-1) in
    let p = get_vertices g in
    while not (S.is_empty p) do
      invariant { inv g values !next }
      invariant { Fset.subset p.S.contents (vertices g) }
      invariant { Fset.subset (Fset.diff (vertices g) p.S.contents) (defined_sort values) }
      variant { S.cardinal p }
      let u = S.choose_and_remove p in
      dfs g u SA.empty values next
    done;
    values

end

module Online_graph
  use export Graph

  val function add_edge (g: graph) (u v: vertex): graph
    ensures { forall x.
      preds result x = if x = v then S.add u (preds g v) else preds g x }
    ensures { forall x.
      succs result x = if x = u then S.add v (succs g u) else succs g x }

end

module Online_Basic

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

  use ref.Ref
  use Online_graph
  use set.Fset

  clone impset.Impset as S with type elt = vertex
  clone appset.Appset as SA with type elt = vertex
  clone import impmap.ImpmapNoDom as M with type key = vertex

  val get_succs (g: graph) (v: vertex): S.t
    ensures { result.S.contents = succs g v }

  exception Cycle_found

  type t = {
    mutable graph : graph;
    mutable values: M.t int;
  }

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

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

  let rec dfs (g: t) (v: vertex) (seen: SA.t) (min_depth: int): unit
    requires { inv g }
    requires { Fset.mem v (vertices g.graph) }
    requires { Fset.subset seen.SA.contents (vertices g.graph) }
    raises  { Cycle_found -> true }
    variant { Fset.cardinal (vertices g.graph) - SA.cardinal seen }
    ensures { min_depth <= g.values[v] }
    ensures { inv g }
    ensures { forall x:vertex. SA.mem x seen -> g.values[x] = old g.values[x] }
    ensures { forall x:vertex. old g.values[x] <= g.values[x] }
  =
    if SA.mem v seen then raise Cycle_found;
    if g.values[v] < min_depth then begin
      let p = get_succs g.graph v in
      let seen = SA.add v seen in
      while not (S.is_empty p) do
        invariant { inv g }
        invariant { forall s:vertex. Fset.mem s (succs g.graph v) -> not (S.mem s p) -> min_depth < g.values[s] }
        invariant { S.subset p.S.contents (succs g.graph v) }
        invariant { forall x:vertex. SA.mem x seen -> g.values[x] = old g.values[x] }
        invariant { forall x:vertex. old g.values[x] <= g.values[x] }
        variant { S.cardinal p }
        let u = S.choose_and_remove p in
        dfs g u seen (min_depth + 1)
      done;
      g.values[v] <- min_depth;
    end

  let add_edge (g: t) (x y: vertex): unit
    requires { inv g }
    requires { Fset.mem x (vertices g.graph) }
    requires { Fset.mem y (vertices g.graph) }
    ensures  { inv g }
    ensures  { g.graph = add_edge (old g.graph) x y }
    raises   { Cycle_found -> true }
  =
    let seen = SA.empty in
    let seen = SA.add x seen in
    dfs g y seen (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

ObligationsCVC4 1.5
VC dfs---
split_goal_right
VC dfs.00.01
VC dfs.10.02
VC dfs.20.05
VC dfs.30.02
VC dfs.40.03
VC dfs.50.02
VC dfs.60.02
VC dfs.70.04
VC dfs.80.02
VC dfs.90.16
VC dfs.100.06
VC dfs.110.06
VC dfs.120.02
VC dfs.130.21
VC dfs.140.03
VC dfs.150.04
VC dfs.160.04
VC dfs.170.02
VC dfs.180.31
VC dfs.190.05
VC dfs.20---
inline_goal
VC dfs.20.0---
split_goal_right
VC dfs.20.0.00.42
VC dfs.20.0.10.04
VC dfs.20.0.2---
inline_goal
VC dfs.20.0.2.00.40
VC dfs.20.0.30.84
VC dfs.210.07
VC dfs.220.03
VC dfs.230.07
VC dfs.240.02
VC dfs.250.02
VC topo_order---
split_goal_right
VC topo_order.0---
inline_goal
VC topo_order.0.0---
split_goal_right
VC topo_order.0.0.00.04
VC topo_order.0.0.10.02
VC topo_order.0.0.20.04
VC topo_order.0.0.30.03
VC topo_order.10.02
VC topo_order.20.03
VC topo_order.30.02
VC topo_order.40.02
VC topo_order.50.04
VC topo_order.60.04
VC topo_order.70.05
VC topo_order.80.02
VC topo_order.90.04
VC topo_order.100.10
VC topo_order.110.01
VC topo_order.120.08

Theory "topological_sorting.Online_Basic": fully verified

ObligationsAlt-Ergo 1.30CVC4 1.5
VC create------
split_goal_right
VC create.0---0.01
VC create.1---0.05
VC dfs------
split_goal_right
VC dfs.0---0.01
VC dfs.1---0.02
VC dfs.2---0.03
VC dfs.3---0.02
VC dfs.4---0.01
VC dfs.5---0.02
VC dfs.6---0.02
VC dfs.7------
split_goal_right
VC dfs.7.0---0.04
VC dfs.7.1---0.04
VC dfs.8---0.02
VC dfs.9---0.12
VC dfs.10---0.06
VC dfs.11---0.06
VC dfs.12---0.02
VC dfs.13---0.08
VC dfs.14---0.04
VC dfs.15---0.05
VC dfs.16---0.05
VC dfs.17---0.01
VC dfs.18---0.04
VC dfs.190.05---
VC dfs.20---0.07
VC dfs.21---0.05
VC dfs.22---0.02
VC dfs.23---0.02
VC dfs.24---0.01
VC dfs.25---0.01
VC add_edge------
split_goal_right
VC add_edge.0---0.02
VC add_edge.1---0.02
VC add_edge.2---0.05
VC add_edge.3---0.19
VC add_edge.4---0.03
VC add_edge.5---0.01