Commit f8909993 by François Bobot

### [Examples] topological sorting static algorithm

parent dc83f5fb
 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 (** direct predecessors *) function preds graph vertex: S.set vertex axiom preds_is_vertices: forall g:graph. forall v:vertex. S.subset (preds g v) (vertices g) type msort = M.map vertex int 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 (preds g v) -> 0 <= (M.get m v) -> 0 <= (M.get m u) < (M.get m v) predicate sort (g: graph) (m:msort) = partial_sort g m /\ forall v:vertex. S.mem v (vertices g) -> 0 <= M.get m v 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 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; assert { inv g !values !next }; assert { not (S.mem v seen) }; 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 let values = ref (M.const (-1)) in 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 end \ No newline at end of file