examples/vstte12_bfs.mlw

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