binary_search2.mlw 571 Bytes
Newer Older
1 2 3 4 5 6 7 8

(* yet another binary search *)

module BinarySearch

  use import int.Int
  use import int.ComputerDivision

Andrei Paskevich's avatar
Andrei Paskevich committed
9
  function f int : int
10 11 12

  axiom f_monotonic : forall x y : int. x <= y -> f x <= f y

13 14 15 16 17
  let rec binary_search target lo hi variant { hi-lo }
    requires { f lo < target <= f hi }
    ensures  { f result >= target /\
      forall x : int. x < result -> f x < target }
  = if lo < hi-1 then
18
      let mid = div (lo + hi) 2 in
19 20 21
      if f mid < target then
        binary_search target mid hi
      else
22 23 24 25 26
        binary_search target lo mid
    else
      hi

end