vstte12_bfs.mlw 4.05 KB
Newer Older
1

Jean-Christophe's avatar
Jean-Christophe committed
2
(* The 2nd Verified Software Competition (VSTTE 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's avatar
Jean-Christophe committed
10 11
  use import int.Int
  use export set.Fset
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
53 54
  use impset.Impset as B
  use import ref.Refint
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 *)
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 /\
84 85
      shortest_path s v !d /\
      (forall x: vertex. x<> v -> closure !visited !current !next x) }
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's avatar
Jean-Christophe committed
90
    while not (B.is_empty acc) do
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)
      }
97
      variant { cardinal !acc }
Jean-Christophe's avatar
Jean-Christophe committed
98
      let w = B.pop acc in
99
      if not (mem w !visited) then begin
Jean-Christophe's avatar
Jean-Christophe committed
100 101
        B.push w visited;
        B.push w next
102 103 104
      end
    done

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 }
108
    diverges (* the set of reachable nodes may be infinite *)
109
  = let visited = ref (singleton s) in
110 111 112
    let current = ref (singleton s) in
    let next    = ref empty in
    let d = ref 0 in
Jean-Christophe's avatar
Jean-Christophe committed
113
    while not (B.is_empty current) do
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's avatar
Jean-Christophe committed
120
      let v = B.pop current in
121 122
      if v = t then raise (Found !d);
      fill_next s t v visited current next d;
Jean-Christophe's avatar
Jean-Christophe committed
123
      if B.is_empty current then begin
124 125 126 127 128 129 130 131
        current := !next;
        next    := empty;
        incr d
      end
    done;
    assert { not (mem t !visited) }

end