Wiki Agenda Contact Version française

Warshall algorithm


Authors: Jean-Christophe Filliâtre / Martin Clochard

Topics: Graph Algorithms

Tools: Why3

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


Warshall algorithm

Computes the transitive closure of a graph implemented as a Boolean matrix.

Authors: Martin Clochard (École Normale Supérieure) Jean-Christophe Filliâtre (CNRS)

module WarshallAlgorithm

  use int.Int
  use matrix.Matrix

  (* path m i j k =
     there is a path from i to j, using only vertices smaller than k *)
  inductive path (matrix bool) int int int =
  | Path_empty:
      forall m: matrix bool, i j k: int.
       m.elts i j -> path m i j k
  | Path_cons:
      forall m: matrix bool, i x j k: int.
      0 <= x < k -> path m i x k -> path m x j k -> path m i j k

  lemma weakening:
    forall m i j k1 k2. 0 <= k1 <= k2 ->
    path m i j k1 -> path m i j k2

  lemma decomposition:
    forall m k. 0 <= k -> forall i j. path m i j (k+1) ->
      (path m i j k \/ (path m i k k /\ path m k j k))

  let transitive_closure (m: matrix bool) : matrix bool
    requires { m.rows = m.columns }
    ensures  { let n = m.rows in
               forall x y: int. 0 <= x < n -> 0 <= y < n ->
               result.elts x y <-> path m x y n }
  =
    let t = copy m in
    let n = m.rows in
    for k = 0 to n - 1 do
      invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
                  t.elts x y <-> path m x y k }
      for i = 0 to n - 1 do
        invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
                    t.elts x y <->
                    if x < i
                    then path m x y (k+1)
                    else path m x y k }
        for j = 0 to n - 1 do
          invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
                      t.elts x y <->
                      if x < i \/ (x = i /\ y < j)
                      then path m x y (k+1)
                      else path m x y k }
          set t i j (get t i j || get t i k && get t k j)
        done
      done
    done;
    t

end

download ZIP archive

Why3 Proof Results for Project "warshall_algorithm"

Theory "warshall_algorithm.WarshallAlgorithm": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5Coq 8.11.2Z3 4.12.2
weakening------------
induction_pr
weakening.00.00---------
weakening.1---0.01------
decomposition------0.96---
VC for transitive_closure------------
split_goal_right
loop invariant init0.00---------
loop invariant init0.00---------
loop invariant init0.01---------
index in matrix bounds0.00---------
index in matrix bounds0.00---------
index in matrix bounds0.00---------
index in matrix bounds0.00---------
loop invariant preservation------------
split_goal_right
loop invariant preservation0.14---------
loop invariant preservation0.03---------
loop invariant preservation---------0.02
loop invariant preservation0.01---------
loop invariant preservation0.00---------
loop invariant preservation0.00---------
loop invariant preservation0.00---------
postcondition0.00---------
out of loop bounds0.00---------