examples/warshall_algorithm.mlw

   1
   2 (** Warshall algorithm
   3
   4     Computes the transitive closure of a graph implemented as a Boolean
   5     matrix.
   6
   7     Authors: Martin Clochard (École Normale Supérieure)
   8              Jean-Christophe Filliâtre (CNRS)
   9  *)
  10
  11 module WarshallAlgorithm
  12
  13   use int.Int
  14   use matrix.Matrix
  15
  16   (* path m i j k =
  17      there is a path from i to j, using only vertices smaller than k *)
  18   inductive path (matrix bool) int int int =
  19   | Path_empty:
  20       forall m: matrix bool, i j k: int.
  21        m.elts i j -> path m i j k
  22   | Path_cons:
  23       forall m: matrix bool, i x j k: int.
  24       0 <= x < k -> path m i x k -> path m x j k -> path m i j k
  25
  26   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   let transitive_closure (m: matrix bool) : matrix bool
  35     requires { m.rows = m.columns }
  36     ensures  { let n = m.rows in
  37                forall x y: int. 0 <= x < n -> 0 <= y < n ->
  38                result.elts x y <-> path m x y n }
  39   =
  40     let t = copy m in
  41     let n = m.rows in
  42     for k = 0 to n - 1 do
  43       invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
  44                   t.elts x y <-> path m x y k }
  45       for i = 0 to n - 1 do
  46         invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
  47                     t.elts x y <->
  48                     if x < i
  49                     then path m x y (k+1)
  50                     else path m x y k }
  51         for j = 0 to n - 1 do
  52           invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
  53                       t.elts x y <->
  54                       if x < i \/ (x = i /\ y < j)
  55                       then path m x y (k+1)
  56                       else path m x y k }
  57           set t i j (get t i j || get t i k && get t k j)
  58         done
  59       done
  60     done;
  61     t
  62
  63 end