mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
64 lines
1.8 KiB
Plaintext
64 lines
1.8 KiB
Plaintext
|
|
(** 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
|