vstte12_bfs.mlw 4.05 KB
 Jean-Christophe committed Jan 29, 2012 1 `````` `````` Jean-Christophe committed Apr 01, 2012 2 ``````(* The 2nd Verified Software Competition (VSTTE 2012) `````` Jean-Christophe committed Jan 29, 2012 3 4 5 6 7 8 9 `````` https://sites.google.com/site/vstte2012/compet Problem 5: Shortest path in a graph using breadth-first search *) theory Graph `````` Jean-Christophe committed Apr 01, 2012 10 11 `````` use import int.Int use export set.Fset `````` Jean-Christophe committed Jan 29, 2012 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 `````` type vertex function succ vertex : set vertex (* there is a path of length n from v1 to v2 *) inductive path (v1 v2: vertex) (n: int) = | path_empty: forall v: vertex. path v v 0 | path_succ: forall v1 v2 v3: vertex, n: int. path v1 v2 n -> mem v3 (succ v2) -> path v1 v3 (n+1) (* path length is non-negative *) lemma path_nonneg: forall v1 v2: vertex, n: int. path v1 v2 n -> n >= 0 (* a non-empty path has a last but one node *) lemma path_inversion: forall v1 v3: vertex, n: int. n >= 0 -> path v1 v3 (n+1) -> exists v2: vertex. path v1 v2 n /\ mem v3 (succ v2) (* a path starting in a set S that is closed under succ ends up in S *) lemma path_closure: forall s: set vertex. (forall x: vertex. mem x s -> forall y: vertex. mem y (succ x) -> mem y s) -> forall v1 v2: vertex, n: int. path v1 v2 n -> mem v1 s -> mem v2 s predicate shortest_path (v1 v2: vertex) (n: int) = path v1 v2 n /\ forall m: int. m < n -> not (path v1 v2 m) end module BFS use import int.Int use import Graph `````` Andrei Paskevich committed Oct 13, 2012 53 54 `````` use impset.Impset as B use import ref.Refint `````` Jean-Christophe committed Jan 29, 2012 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` exception Found int (* global invariant *) predicate inv (s t: vertex) (visited current next: set vertex) (d: int) = (* current *) subset current visited /\ (forall x: vertex. mem x current -> shortest_path s x d) /\ (* next *) subset next visited /\ (forall x: vertex. mem x next -> shortest_path s x (d + 1)) /\ (* visited *) (forall x: vertex, m: int. path s x m -> m <= d -> mem x visited) /\ (forall x: vertex. mem x visited -> exists m: int. path s x m /\ m <= d+1) /\ (* nodes at distance d+1 are either in next or not yet visited *) (forall x: vertex. shortest_path s x (d + 1) -> mem x next \/ not (mem x visited)) /\ (* target t *) (mem t visited -> mem t current \/ mem t next) (* visited\current\next is closed under succ *) predicate closure (visited current next: set vertex) (x: vertex) = mem x visited -> not (mem x current) -> not (mem x next) -> forall y: vertex. mem y (succ x) -> mem y visited (* function fill_next fills set next with the unvisited successors of v *) `````` Andrei Paskevich committed Oct 13, 2012 82 83 `````` let fill_next (s t v: vertex) (visited current next: B.t vertex) (d:ref int) requires { inv s t !visited !current !next !d /\ `````` Jean-Christophe committed Jan 29, 2012 84 85 `````` shortest_path s v !d /\ (forall x: vertex. x<> v -> closure !visited !current !next x) } `````` Andrei Paskevich committed Oct 13, 2012 86 87 88 89 `````` ensures { inv s t !visited !current !next !d /\ subset (succ v) !visited /\ (forall x: vertex. closure !visited !current !next x) } = let acc = ref (succ v) in `````` Jean-Christophe committed Apr 01, 2012 90 `````` while not (B.is_empty acc) do `````` Jean-Christophe committed Jan 29, 2012 91 92 93 94 95 96 `````` invariant { inv s t !visited !current !next !d /\ subset !acc (succ v) /\ subset (diff (succ v) !acc) !visited /\ (forall x: vertex. x<> v -> closure !visited !current !next x) } `````` MARCHE Claude committed Feb 03, 2014 97 `````` variant { cardinal !acc } `````` Jean-Christophe committed Apr 01, 2012 98 `````` let w = B.pop acc in `````` Jean-Christophe committed Jan 29, 2012 99 `````` if not (mem w !visited) then begin `````` Jean-Christophe committed Apr 01, 2012 100 101 `````` B.push w visited; B.push w next `````` Jean-Christophe committed Jan 29, 2012 102 103 104 `````` end done `````` Andrei Paskevich committed Oct 13, 2012 105 106 107 `````` let bfs (s: vertex) (t: vertex) ensures { forall d: int. not (path s t d) } raises { Found r -> shortest_path s t r } `````` Jean-Christophe Filliatre committed Feb 19, 2014 108 `````` diverges (* the set of reachable nodes may be infinite *) `````` Andrei Paskevich committed Oct 13, 2012 109 `````` = let visited = ref (singleton s) in `````` Jean-Christophe committed Jan 29, 2012 110 111 112 `````` let current = ref (singleton s) in let next = ref empty in let d = ref 0 in `````` Jean-Christophe committed Apr 01, 2012 113 `````` while not (B.is_empty current) do `````` Jean-Christophe committed Jan 29, 2012 114 115 116 117 118 119 `````` invariant { inv s t !visited !current !next !d /\ (is_empty !current -> is_empty !next) /\ (forall x: vertex. closure !visited !current !next x) /\ 0 <= !d } `````` Jean-Christophe committed Apr 01, 2012 120 `````` let v = B.pop current in `````` Jean-Christophe committed Jan 29, 2012 121 122 `````` if v = t then raise (Found !d); fill_next s t v visited current next d; `````` Jean-Christophe committed Apr 01, 2012 123 `````` if B.is_empty current then begin `````` Jean-Christophe committed Jan 29, 2012 124 125 126 127 128 129 130 131 `````` current := !next; next := empty; incr d end done; assert { not (mem t !visited) } end``````