examples_in_progress/binary_search2.mlw

   1
   2 (* yet another binary search *)
   3
   4 module BinarySearch
   5
   6   use int.Int
   7   use int.ComputerDivision
   8
   9   val function f int : int
  10
  11   axiom f_monotonic : forall x y : int. x <= y -> f x <= f y
  12
  13   let rec binary_search target lo hi variant { hi-lo }
  14     requires { f lo < target <= f hi }
  15     ensures  { f result >= target /\
  16       forall x : int. x < result -> f x < target }
  17   = if lo < hi-1 then
  18       let mid = div (lo + hi) 2 in
  19       if f mid < target then
  20         binary_search target mid hi
  21       else
  22         binary_search target lo mid
  23     else
  24       hi
  25
  26 end