examples_in_progress/binary_search_c.mlw

   1
   2 (* We illustrate the use of Why for the verification of C programs on
   3    "the challenge of binary search" (Jon Bentley's Programming Pearls).
   4
   5 int binary_search(int* t, int n, int v) {
   6   int l = 0, u = n-1;
   7   while (l <= u) {
   8     int m = (l + u) / 2;
   9     if (t[m] < v)
  10       l = m + 1;
  11     else if (t[m] > v)
  12       u = m - 1;
  13     else
  14       return m;
  15   }
  16   return -1;
  17
  18 *)
  19
  20 module M1
  21
  22   use int.Int
  23   use int.ComputerDivision
  24   use ref.Ref
  25
  26   type pointer
  27   type memory
  28   val function get memory pointer int : int
  29
  30   val mem : ref memory
  31
  32   exception Return int
  33
  34   let binary_search (t : pointer) (n : int) (v : int)
  35     requires { forall k1 k2:int.
  36         0 <= k1 <= k2 <= n-1 -> get !mem t k1 <= get !mem t k2 }
  37     ensures  { (result >= 0 /\ get !mem t result = v) \/
  38       (result = -1 /\ forall k:int. 0<=k<n -> get !mem t k <> v) }
  39   = try
  40       let l = ref 0 in
  41       let u = ref (n-1) in
  42       while !l <= !u do
  43         invariant { 0 <= !l /\ !u <= n-1 }
  44         invariant {
  45           forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
  46         variant { !u - !l }
  47         let m = div (!l + !u) 2 in
  48         if get !mem t m < v then l := m + 1
  49         else if get !mem t m > v then u := m - 1
  50         else raise (Return m)
  51       done;
  52       raise (Return (-1))
  53     with Return r ->
  54       r
  55     end
  56
  57 end
  58
  59 (* next step: we want to add array bound checking
  60
  61    to do so, we
  62    1. introduce the notion of blocksize in the model
  63    2. add a program function "get_" with a precondition, to be used in the code
  64       (instead of the pure function "get")
  65 *)
  66
  67 module M2
  68
  69   use int.Int
  70   use int.ComputerDivision
  71   use ref.Ref
  72
  73   type pointer
  74   type memory
  75   function get memory pointer int : int
  76
  77   val mem : ref memory
  78
  79   function block_size memory pointer : int
  80
  81   val get_ (p : pointer) (ofs : int) : int
  82     requires { 0 <= ofs < block_size !mem p }
  83     ensures  { result = get !mem p ofs }
  84
  85   exception Return int
  86
  87   let binary_search (t : pointer) (n : int) (v : int)
  88     requires { n <= block_size !mem t }
  89     requires { forall k1 k2:int.
  90         0 <= k1 <= k2 <= n-1 -> get !mem t k1 <= get !mem t k2 }
  91     ensures { (result >= 0 /\ get !mem t result = v) \/
  92       (result = -1 /\ forall k:int. 0<=k<n -> get !mem t k <> v) }
  93   = try
  94       let l = ref 0 in
  95       let u = ref (n-1) in
  96       while !l <= !u do
  97         invariant { 0 <= !l /\ !u <= n-1 }
  98         invariant {
  99           forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
 100         variant { !u - !l }
 101         let m = div (!l + !u) 2 in
 102         if get_ t m < v then l := m + 1
 103         else if get_ t m > v then u := m - 1
 104         else raise (Return m)
 105       done;
 106       raise (Return (-1))
 107     with Return r ->
 108       r
 109     end
 110 end
 111
 112 (* Finally, let us prove the absence of arithmetic overflow
 113 *)
 114
 115 module M3
 116
 117   use int.Int
 118   use int.ComputerDivision
 119   use ref.Ref
 120
 121   type int32
 122   val function to_int int32 : int
 123
 124   axiom int32_domain : forall x:int32. -2147483648 <= to_int x <= 2147483647
 125
 126   val of_int (x:int) : int32
 127     requires { -2147483648 <= x <= 2147483647 }
 128     ensures  { to_int result = x }
 129
 130   type pointer
 131   type memory
 132   function get memory pointer int : int32
 133
 134   val mem : ref memory
 135
 136   function block_size memory pointer : int
 137
 138   val get_ (p:pointer) (ofs:int32) : int32
 139     requires { 0 <= to_int ofs < block_size !mem p }
 140     ensures  { result = get !mem p (to_int ofs) }
 141
 142   exception Return int32
 143
 144   let binary_search (t : pointer) (n : int32) (v : int32)
 145     requires { 0 <= to_int n <= block_size !mem t }
 146     requires { forall k1 k2:int.
 147         0 <= k1 <= k2 <= to_int n - 1 ->
 148         to_int (get !mem t k1) <= to_int (get !mem t k2) }
 149     ensures  { (to_int result >= 0 /\
 150        to_int (get !mem t (to_int result)) = to_int v)
 151       \/
 152       (to_int result = -1 /\
 153        forall k:int. 0<=k<to_int n -> to_int (get !mem t k) <> to_int v) }
 154   = try
 155       let l = ref (of_int 0) in
 156       let u = ref (of_int (to_int n - to_int (of_int 1))) in
 157       while to_int !l <= to_int !u do
 158         invariant { 0 <= to_int !l /\ to_int !u <= to_int n - 1 }
 159         invariant { forall k:int. 0 <= k < to_int n ->
 160           to_int (get !mem t k) = to_int v -> to_int !l <= k <= to_int !u }
 161         variant { to_int !u - to_int !l }
 162         let m = of_int (to_int !l
 163                         +
 164                         to_int
 165                           (of_int
 166                              (div (to_int (of_int (to_int !u - to_int !l)))
 167                                   (to_int (of_int 2)))))
 168         in
 169         if to_int (get_ t m) < to_int v then l := of_int (to_int m + 1)
 170         else if to_int (get_ t m) > to_int v then u := of_int (to_int m - 1)
 171         else raise (Return m)
 172       done;
 173       raise (Return (of_int (-1)))
 174     with Return r ->
 175       r
 176     end
 177 end