topological_sorting.mlw 6.43 KB
 Jean-Christophe Filliatre committed Sep 02, 2014 1 2 3 4 5 6 `````` (** Topological sorting Author: François Bobot (CEA) *) `````` François Bobot committed Jul 20, 2014 7 8 9 10 11 12 13 14 15 16 17 18 ``````theory Graph use export int.Int use set.Fset as S use map.Map as M (* the graph is defined by a set of vertices and a set of edges *) type vertex type graph function vertices graph: S.set vertex `````` François Bobot committed Jul 21, 2014 19 20 21 22 23 24 `````` function edges graph: S.set (vertex , vertex) axiom edges_use_vertices: forall g:graph. forall x y:vertex. S.mem (x,y) (edges g) -> (S.mem x (vertices g) /\ S.mem y (vertices g)) `````` François Bobot committed Jul 20, 2014 25 26 27 `````` (** direct predecessors *) function preds graph vertex: S.set vertex `````` François Bobot committed Jul 21, 2014 28 29 `````` axiom preds_def: forall g:graph. forall v:vertex. forall u:vertex. S.mem (u,v) (edges g) <-> S.mem u (preds g v) `````` François Bobot committed Jul 20, 2014 30 `````` `````` François Bobot committed Jul 21, 2014 31 32 33 34 `````` (** direct successors *) function succs graph vertex: S.set vertex axiom succs_def: forall g:graph. forall v:vertex. forall u:vertex. S.mem (u,v) (edges g) <-> S.mem v (succs g u) `````` François Bobot committed Jul 20, 2014 35 `````` `````` François Bobot committed Jul 21, 2014 36 `````` type msort = M.map vertex int `````` François Bobot committed Jul 20, 2014 37 38 `````` predicate sort (g: graph) (m:msort) = `````` François Bobot committed Jul 21, 2014 39 40 41 `````` forall v:vertex. forall u:vertex. S.mem (u,v) (edges g) -> (M.get m u) < (M.get m v) `````` François Bobot committed Jul 20, 2014 42 43 44 45 46 47 48 49 50 51 `````` end (** static topological sorting by depth-first search *) module Static use import ref.Ref use import Graph use set.Fset as S use map.Map as M `````` MARCHE Claude committed Jul 06, 2015 52 `````` use map.Const `````` François Bobot committed Jul 20, 2014 53 `````` `````` François Bobot committed Jul 21, 2014 54 55 56 57 58 59 60 61 62 63 `````` function defined_sort (m:msort) : S.set vertex axiom defined_sort_def: forall m:msort. forall v: vertex[S.mem v (defined_sort m)]. S.mem v (defined_sort m) <-> 0 <= M.get m v predicate partial_sort (g: graph) (m:msort) = forall v:vertex. forall u:vertex. S.mem (u,v) (edges g) -> 0 <= (M.get m v) -> 0 <= (M.get m u) < (M.get m v) `````` François Bobot committed Jul 20, 2014 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 `````` type marked = (S.set vertex) exception Cycle_found predicate inv (g:graph) (m:msort) (next:int) = S.subset (defined_sort m) (vertices g) && 0 <= next && partial_sort g m && forall v:vertex. S.mem v (defined_sort m) -> M.get m v < next let rec dfs (g:graph) (v:vertex) (seen:marked) (values:ref msort) (next: ref int) : unit requires { inv g !values !next } requires { S.mem v (vertices g) } requires { S.subset seen (vertices g) } variant { S.cardinal (vertices g) - S.cardinal seen } ensures { S.subset (old (defined_sort !values)) (defined_sort !values) } ensures { 0 <= M.get !values v <= !next} ensures { inv g !values !next } ensures { forall x:vertex. S.mem x seen -> M.get (old !values) x = M.get !values x } raises { Cycle_found -> true } = 'Init: if S.mem v seen then raise Cycle_found; if not (0 <= M.get !values v) then 'Init_loop: begin let p = ref (preds g v) in let seen = S.add v seen in while not (S.is_empty !p) do invariant { inv g !values !next } invariant { S.subset (S.diff (preds g v) !p) (defined_sort !values) } invariant { S.subset (at (defined_sort !values) 'Init) (defined_sort !values) } invariant { S.subset !p (preds g v) } invariant { forall x:vertex. S.mem x seen -> M.get (at !values 'Init_loop) x = M.get !values x } variant {S.cardinal !p} let u = S.choose !p in dfs g u seen values next; p := S.remove u !p done; end; values := M.set !values v !next; next := !next + 1 let topo_order (g:graph): msort raises { Cycle_found -> true } ensures { sort g result } = 'Init: let next = ref 0 in `````` MARCHE Claude committed Jul 06, 2015 114 `````` let values = ref (Const.const (-1)) in `````` François Bobot committed Jul 20, 2014 115 116 117 118 119 120 121 122 123 124 125 126 127 `````` let p = ref (vertices g) in while not (S.is_empty !p) do invariant { inv g !values !next } invariant { S.subset !p (vertices g) } invariant { S.subset (S.diff (vertices g) !p) (defined_sort !values) } invariant { S.subset (at (defined_sort !values) 'Init) (defined_sort !values) } variant {S.cardinal !p} let u = S.choose !p in dfs g u (S.empty) values next; p := S.remove u !p done; !values `````` François Bobot committed Jul 21, 2014 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 ``````end module Online_graph use export Graph function add_edge graph vertex vertex: graph axiom add_edge_def_preds: forall g:graph. forall u v:vertex. forall x. preds (add_edge g u v) x = if x = v then S.add u (preds g v) else preds g x axiom add_edge_def_succs: forall g:graph. forall u v:vertex. forall x. succs (add_edge g u v) x = if x = u then S.add v (succs g u) else succs g x end (** A New Approach to Incremental Topological Ordering Michael A. Bender, Jeremy T. Fineman, Seth Gilbert *) module Online_Basic use import ref.Ref use import Online_graph use set.Fset as S use map.Map as M `````` MARCHE Claude committed Jul 06, 2015 159 `````` use map.Const `````` François Bobot committed Jul 21, 2014 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 `````` type marked = (S.set vertex) exception Cycle_found type t = { mutable graph : graph; mutable values: msort; } predicate inv (g:t) = sort g.graph g.values let create (g:graph): t requires { forall x: vertex. S.is_empty (preds g x) } ensures { result.graph = g } ensures { inv result } = `````` MARCHE Claude committed Jul 06, 2015 177 `````` {graph = g; values = Const.const 0} `````` François Bobot committed Jul 21, 2014 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 `````` let rec dfs (g:t) (v:vertex) (seen:marked) (min_depth:int) : unit requires { inv g } requires { S.mem v (vertices g.graph) } requires { S.subset seen (vertices g.graph) } raises { Cycle_found -> true } variant { S.cardinal (vertices g.graph) - S.cardinal seen } ensures { min_depth <= M.get g.values v} ensures { inv g } ensures { forall x:vertex. S.mem x seen -> M.get (old g.values) x = M.get g.values x } ensures { forall x:vertex. M.get (old g.values) x <= M.get g.values x } = 'Init: if S.mem v seen then raise Cycle_found; if M.get g.values v < min_depth then 'Init_loop: begin let p = ref (succs g.graph v) in let seen = S.add v seen in while not (S.is_empty !p) do invariant { inv g } invariant { forall s:vertex. S.mem s (succs g.graph v) -> not (S.mem s !p) -> min_depth < M.get g.values s } invariant { S.subset !p (succs g.graph v) } invariant { forall x:vertex. S.mem x seen -> M.get (at g.values 'Init_loop) x = M.get g.values x } invariant { forall x:vertex. M.get (at g.values 'Init_loop) x <= M.get g.values x } variant {S.cardinal !p} let u = S.choose !p in dfs g u seen (min_depth + 1); p := S.remove u !p done; end; g.values <- M.set g.values v min_depth let add_edge (g:t) (x:vertex) (y:vertex): unit requires { inv g } requires { S.mem x (vertices g.graph) } requires { S.mem y (vertices g.graph) } ensures { inv g } ensures { g.graph = old (add_edge g.graph x y) } raises { Cycle_found -> true } = dfs g y (S.singleton x) (M.get g.values x + 1); g.graph <- add_edge g.graph x y; end``````