bench/infer/binary_search.mlw

   1 (* Binary search
   2
   3    A classical example. Searches a sorted array for a given value v. *)
   4
   5 module BinarySearch
   6
   7   use int.Int
   8   use int.ComputerDivision
   9   use ref.Ref
  10   use array.Array
  11
  12   (* the code and its specification *)
  13
  14   exception Break int (* raised to exit the loop *)
  15   exception Not_found (* raised to signal a search failure *)
  16
  17   val mydiv(x:int):int
  18   ensures { 2*result = x }
  19
  20   let binary_search [@bddinfer] [@infer](a : array int) (v : int)
  21     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
  22     ensures  { 0 <= result < length a /\ a[result] = v }
  23     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  24   = try
  25       let l = ref 0 in
  26           l := 0;
  27       let u = ref (length a - 1) in
  28       while !l <= !u do
  29         invariant { !u < length a }
  30         invariant {
  31           forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
  32         variant { !u - !l }
  33         let m = !l + mydiv (!u - !l)  in
  34         assert { !l <= m <= !u };
  35         if a[m] < v then
  36           l := m + 1
  37         else if a[m] > v then
  38           u := m - 1
  39         else
  40           raise (Break m)
  41       done;
  42       raise Not_found
  43     with Break i ->
  44       i
  45     end
  46
  47   let binary_search2 [@bddinfer] [@infer:oct](a : array int) (v : int)
  48     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
  49     ensures  { 0 <= result < length a /\ a[result] = v }
  50     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  51   = try
  52       let l = ref 0 in
  53           l := 0;
  54       let u = ref (length a - 1) in
  55       while !l <= !u do
  56         invariant { !u < length a }
  57         invariant {
  58           forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
  59         variant { !u - !l }
  60         let m = !l + mydiv (!u - !l)  in
  61         assert { !l <= m <= !u };
  62         if a[m] < v then
  63           l := m + 1
  64         else if a[m] > v then
  65           u := m - 1
  66         else
  67           raise (Break m)
  68       done;
  69       raise Not_found
  70     with Break i ->
  71       i
  72     end
  73
  74   let binary_search3 [@bddinfer] [@infer:box](a : array int) (v : int)
  75     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
  76     ensures  { 0 <= result < length a /\ a[result] = v }
  77     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  78   = try
  79       let l = ref 0 in
  80           l := 0;
  81       let u = ref (length a - 1) in
  82       while !l <= !u do
  83         invariant { !u < length a }
  84         invariant {
  85           forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
  86         variant { !u - !l }
  87         let m = !l + mydiv (!u - !l)  in
  88         assert { !l <= m <= !u };
  89         if a[m] < v then
  90           l := m + 1
  91         else if a[m] > v then
  92           u := m - 1
  93         else
  94           raise (Break m)
  95       done;
  96       raise Not_found
  97     with Break i ->
  98       i
  99     end
 100
 101 end