## Warshall algorithm

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

 Obligations Alt-Ergo 2.0.0 CVC4 1.5 Coq 8.11.2 Z3 4.12.2 weakening --- --- --- --- induction_pr weakening.0 0.00 --- --- --- weakening.1 --- 0.01 --- --- decomposition --- --- 0.96 --- VC for transitive_closure --- --- --- --- split_goal_right loop invariant init 0.00 --- --- --- loop invariant init 0.00 --- --- --- loop invariant init 0.01 --- --- --- index in matrix bounds 0.00 --- --- --- index in matrix bounds 0.00 --- --- --- index in matrix bounds 0.00 --- --- --- index in matrix bounds 0.00 --- --- --- loop invariant preservation --- --- --- --- split_goal_right loop invariant preservation 0.14 --- --- --- loop invariant preservation 0.03 --- --- --- loop invariant preservation --- --- --- 0.02 loop invariant preservation 0.01 --- --- --- loop invariant preservation 0.00 --- --- --- loop invariant preservation 0.00 --- --- --- loop invariant preservation 0.00 --- --- --- postcondition 0.00 --- --- --- out of loop bounds 0.00 --- --- ---