examples/search.mlw

   1
   2 (** Search Algorithms
   3
   4     Author: Jean-Christophe Filliâtre (CNRS)
   5 *)
   6
   7 module Path
   8
   9   use export int.Int
  10   use export seq.Seq
  11
  12   type state
  13
  14   val function moves (s: state) : seq state
  15
  16   val constant start: state
  17
  18   val predicate success (s: state)
  19
  20   inductive path state state int =
  21   | Path0: forall s. path s s 0
  22   | Path1: forall s i. 0 <= i < length (moves s) ->
  23            path s (moves s)[i] 1
  24   | Patht: forall s t u n m. path s t n -> path t u m -> path s u (n+m)
  25
  26   predicate move (s t: state) =
  27     exists i. 0 <= i < length (moves s) /\ t = (moves s)[i]
  28
  29   let lemma path_inversion (s t: state) (n: int)
  30     requires { path s t n }
  31     ensures  { n = 0 /\ s = t
  32             \/ n > 0 /\ exists i. 0 <= i < length (moves s) /\
  33                         path (moves s)[i] t (n-1) }
  34   = () (* by induction_pr *)
  35
  36   let lemma path_length (s t: state) (n: int)
  37     requires { path s t n } ensures { n >= 0 }
  38   = ()
  39
  40   let lemma path_first (s t: state) (n: int) : (s': state)
  41     requires { path s t n } requires { n > 0 }
  42     ensures  { move s s' }
  43     ensures  { path s' t (n-1) }
  44   = for i = 0 to length (moves s) - 1 do
  45       invariant { forall j. 0 <= j < i -> not (path (moves s)[j] t (n-1)) }
  46       let s' = (moves s)[i] in
  47       if path s' t (n-1) then return s';
  48     done;
  49     absurd
  50
  51   let rec lemma path_inversion_right (s t: state) (n: int)
  52     requires { path s t n }
  53     ensures  { n = 0 /\ s = t
  54             \/ n > 0 /\ exists s'. path s s' (n-1) /\ move s' t }
  55     variant  { n }
  56   = if n > 0 then path_inversion_right (path_first s t n) t (n-1)
  57
  58   let rec lemma path_last (s t: state) (n: int) : (t': state)
  59     requires { path s t n } requires { n > 0 }
  60     ensures  { path s t' (n-1) } ensures { move t' t }
  61     variant  { n }
  62   = if n = 1 then s else path_last (path_first s t n) t (n-1)
  63
  64   let rec lemma shorter_path (s t: state) (n m: int) : (r: state)
  65     requires { path s t n } requires { 0 <= m <= n }
  66     ensures  { path s r m }
  67     variant  { n }
  68   = if n = 0 || m = 0 then s else shorter_path (path_first s t n) t (n-1) (m-1)
  69
  70   type outcome =
  71     | NoSolution
  72     | Solution state int
  73
  74 end
  75
  76 module Bfs
  77
  78   use Path
  79   use seq.Mem
  80
  81   let bfs () : (o: outcome)
  82     ensures  { match o with
  83                | NoSolution -> forall t n. success t -> not (path start t n)
  84                | Solution t n -> path start t n
  85                end }
  86     diverges
  87   = let ref cur = cons start empty in
  88     let ref p = 0 in
  89     while length cur > 0 do
  90       invariant { p >= 0 }
  91       invariant { forall i. 0 <= i < length cur -> path start cur[i] p }
  92       invariant { forall t. path start t p -> mem t cur }
  93       invariant { forall t n. path start t n -> success t -> n >= p }
  94       let ref nxt = empty in
  95       for i = 0 to length cur - 1 do
  96         invariant { forall l. 0 <= l < length nxt ->
  97                     exists j. 0 <= j < i /\ move cur[j] nxt[l] }
  98         invariant { forall j k. 0 <= j < i -> 0 <= k < length (moves cur[j]) ->
  99                     mem (moves cur[j])[k] nxt }
 100         invariant { forall j. 0 <= j < i -> not (success cur[j]) }
 101         let s = cur[i] in
 102         if success s then return (Solution s p);
 103         nxt <- moves s ++ nxt
 104       done;
 105       cur <- nxt;
 106       p <- p+1
 107     done;
 108     return NoSolution
 109
 110 end
 111
 112 module Dfs
 113
 114   use Path
 115
 116   let rec dfs (m: int) (s: state) (p: int) : (o: outcome)
 117     requires { 0 <= p <= m+1 }
 118     ensures  { match o with
 119                | NoSolution   -> forall t n.
 120                                  0 <= n <= m-p -> success t -> not (path s t n)
 121                | Solution t n -> path s t n /\ success t /\ 0 <= n <= m-p
 122                end }
 123     variant  { m - p }
 124   = if p > m then return NoSolution;
 125     if success s then return (Solution s 0);
 126     let mv = moves s in
 127     for i = 0 to length mv - 1 do
 128       invariant { forall j t n. 0 <= j < i -> path mv[j] t n ->
 129                   success t -> 0 <= n < m-p -> false }
 130       match dfs m mv[i] (p+1) with
 131         | Solution t n -> return (Solution t (n+1))
 132         | NoSolution   -> ()
 133       end
 134     done;
 135     return NoSolution
 136
 137   let dfs_max (m: int) : (o: outcome)
 138     requires { 0 <= m }
 139     ensures  { match o with
 140                | NoSolution -> forall t n.
 141                                0 <= n <= m -> success t -> not (path start t n)
 142                | Solution t n -> path start t n /\ n <= m
 143                end }
 144   = dfs m start 0
 145
 146 end