warshall_algorithm.mlw 1.85 KB
 Jean-Christophe Filliatre committed May 17, 2014 1 2 3 4 `````` (** Warshall algorithm Computes the transitive closure of a graph implemented as a Boolean `````` Jean-Christophe Filliatre committed May 26, 2014 5 6 7 8 9 `````` matrix. Authors: Martin Clochard (École Normale Supérieure) Jean-Christophe Filliâtre (CNRS) *) `````` Jean-Christophe Filliatre committed May 17, 2014 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. `````` Jean-Christophe Filliatre committed Jul 06, 2015 21 `````` get m i j -> path m i j k `````` Jean-Christophe Filliatre committed May 17, 2014 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: `````` Martin Clochard committed May 26, 2014 27 `````` forall m i j k1 k2. 0 <= k1 <= k2 -> `````` Jean-Christophe Filliatre committed May 17, 2014 28 `````` path m i j k1 -> path m i j k2 `````` Jean-Christophe Filliatre committed May 26, 2014 29 `````` `````` Martin Clochard committed May 26, 2014 30 `````` lemma decomposition: `````` Jean-Christophe Filliatre committed May 26, 2014 31 `````` forall m k. 0 <= k -> forall i j. path m i j (k+1) -> `````` Martin Clochard committed May 26, 2014 32 `````` (path m i j k \/ (path m i k k /\ path m k j k)) `````` Jean-Christophe Filliatre committed May 17, 2014 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 -> `````` Jean-Christophe Filliatre committed Jul 06, 2015 38 `````` get result x y <-> path m x y n } `````` Jean-Christophe Filliatre committed May 17, 2014 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 -> `````` Jean-Christophe Filliatre committed Jul 06, 2015 44 `````` get t x y <-> path m x y k } `````` Jean-Christophe Filliatre committed May 17, 2014 45 46 `````` for i = 0 to n - 1 do invariant { forall x y. 0 <= x < n -> 0 <= y < n -> `````` Jean-Christophe Filliatre committed Jul 06, 2015 47 `````` get t x y <-> `````` Martin Clochard committed May 26, 2014 48 49 50 `````` if x < i then path m x y (k+1) else path m x y k } `````` Jean-Christophe Filliatre committed May 17, 2014 51 52 `````` for j = 0 to n - 1 do invariant { forall x y. 0 <= x < n -> 0 <= y < n -> `````` Jean-Christophe Filliatre committed Jul 06, 2015 53 `````` get t x y <-> `````` Martin Clochard committed May 26, 2014 54 55 56 `````` if x < i \/ (x = i /\ y < j) then path m x y (k+1) else path m x y k } `````` Jean-Christophe Filliatre committed Jul 06, 2015 57 `````` set t i j (get t i j || get t i k && get t k j) `````` Jean-Christophe Filliatre committed May 17, 2014 58 59 60 61 62 63 `````` done done done; t end``````