warshall_algorithm.mlw 1.85 KB
Newer Older
1 2 3 4

(** Warshall algorithm

    Computes the transitive closure of a graph implemented as a Boolean
5 6 7 8 9
    matrix.

    Authors: Martin Clochard (École Normale Supérieure)
             Jean-Christophe Filliâtre (CNRS)
 *)
10 11 12 13 14 15 16 17 18 19 20

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.
21
      get m i j -> path m i j k
22 23 24 25 26
  | 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:
27
    forall m i j k1 k2. 0 <= k1 <= k2 ->
28
    path m i j k1 -> path m i j k2
29

30
  lemma decomposition:
31
    forall m k. 0 <= k -> forall i j. path m i j (k+1) ->
32
      (path m i j k \/ (path m i k k /\ path m k j k))
33 34 35 36 37

  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 ->
38
               get result x y <-> path m x y n }
39 40 41 42 43
  =
    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 ->
44
                  get t x y <-> path m x y k }
45 46
      for i = 0 to n - 1 do
        invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
47
                    get t x y <->
48 49 50
                    if x < i
                    then path m x y (k+1)
                    else path m x y k }
51 52
        for j = 0 to n - 1 do
          invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
53
                      get t x y <->
54 55 56
                      if x < i \/ (x = i /\ y < j)
                      then path m x y (k+1)
                      else path m x y k }
57
          set t i j (get t i j || get t i k && get t k j)
58 59 60 61 62 63
        done
      done
    done;
    t

end