## 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 import int.Int use import 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. get m 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 -> get result 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 -> get t x y <-> path m x y k } for i = 0 to n - 1 do invariant { forall x y. 0 <= x < n -> 0 <= y < n -> get t 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 -> get t 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 in 2.89 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | Coq (8.4pl6) | |||

weakening | --- | --- | 0.67 | |||

decomposition | --- | --- | 1.24 | |||

VC for transitive_closure | --- | --- | --- | |||

split_goal_wp | ||||||

1. postcondition | 0.02 | --- | --- | |||

2. loop invariant init | 0.03 | --- | --- | |||

3. loop invariant preservation | 0.02 | --- | --- | |||

4. loop invariant init | 0.08 | --- | --- | |||

5. loop invariant preservation | --- | --- | --- | |||

split_goal_wp | ||||||

1. loop invariant preservation | 0.07 | --- | --- | |||

2. loop invariant preservation | 0.01 | --- | --- | |||

3. loop invariant preservation | 0.00 | --- | --- | |||

6. loop invariant init | 0.06 | --- | --- | |||

7. type invariant | 0.01 | --- | --- | |||

8. index in array bounds | 0.02 | --- | --- | |||

9. index in array bounds | 0.02 | --- | --- | |||

10. loop invariant preservation | --- | --- | --- | |||

split_goal_wp | ||||||

1. loop invariant preservation | --- | --- | --- | |||

split_all_full | ||||||

1. loop invariant preservation | 0.02 | --- | --- | |||

2. loop invariant preservation | 0.03 | --- | --- | |||

2. loop invariant preservation | 0.03 | --- | --- | |||

3. loop invariant preservation | 0.04 | --- | --- | |||

11. index in array bounds | 0.01 | --- | --- | |||

12. index in array bounds | 0.01 | --- | --- | |||

13. index in array bounds | 0.01 | --- | --- | |||

14. loop invariant preservation | --- | --- | --- | |||

split_goal_wp | ||||||

1. loop invariant preservation | --- | 0.03 | --- | |||

2. loop invariant preservation | 0.07 | --- | --- | |||

3. loop invariant preservation | --- | 0.07 | --- | |||

15. index in array bounds | 0.01 | --- | --- | |||

16. loop invariant preservation | --- | --- | --- | |||

split_goal_wp | ||||||

1. loop invariant preservation | --- | 0.03 | --- | |||

2. loop invariant preservation | 0.04 | --- | --- | |||

3. loop invariant preservation | --- | 0.04 | --- | |||

17. loop invariant preservation | 0.10 | --- | --- | |||

18. loop invariant preservation | --- | --- | --- | |||

split_goal_wp | ||||||

1. loop invariant preservation | 0.02 | --- | --- | |||

2. loop invariant preservation | 0.01 | --- | --- | |||

19. type invariant | 0.01 | --- | --- | |||

20. postcondition | 0.06 | --- | --- |