why3/examples_in_progress/binary_search_c.mlw

(* We illustrate the use of Why for the verification of C programs on
   "the challenge of binary search" (Jon Bentley's Programming Pearls).

int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1;
  while (l <= u) {
    int m = (l + u) / 2;
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else
      return m;
  }
  return -1;

*)

module M1

  use int.Int
  use int.ComputerDivision
  use ref.Ref

  type pointer
  type memory
  val function get memory pointer int : int

  val mem : ref memory

  exception Return int

  let binary_search (t : pointer) (n : int) (v : int)
    requires { forall k1 k2:int.
        0 <= k1 <= k2 <= n-1 -> get !mem t k1 <= get !mem t k2 }
    ensures  { (result >= 0 /\ get !mem t result = v) \/
      (result = -1 /\ forall k:int. 0<=k<n -> get !mem t k <> v) }
  = try
      let l = ref 0 in
      let u = ref (n-1) in
      while !l <= !u do
        invariant { 0 <= !l /\ !u <= n-1 }
        invariant {
          forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
        variant { !u - !l }
        let m = div (!l + !u) 2 in
        if get !mem t m < v then l := m + 1
        else if get !mem t m > v then u := m - 1
        else raise (Return m)
      done;
      raise (Return (-1))
    with Return r ->
      r
    end

end

(* next step: we want to add array bound checking

   to do so, we
   1. introduce the notion of blocksize in the model
   2. add a program function "get_" with a precondition, to be used in the code
      (instead of the pure function "get")
*)

module M2

  use int.Int
  use int.ComputerDivision
  use ref.Ref

  type pointer
  type memory
  function get memory pointer int : int

  val mem : ref memory

  function block_size memory pointer : int

  val get_ (p : pointer) (ofs : int) : int
    requires { 0 <= ofs < block_size !mem p }
    ensures  { result = get !mem p ofs }

  exception Return int

  let binary_search (t : pointer) (n : int) (v : int)
    requires { n <= block_size !mem t }
    requires { forall k1 k2:int.
        0 <= k1 <= k2 <= n-1 -> get !mem t k1 <= get !mem t k2 }
    ensures { (result >= 0 /\ get !mem t result = v) \/
      (result = -1 /\ forall k:int. 0<=k<n -> get !mem t k <> v) }
  = try
      let l = ref 0 in
      let u = ref (n-1) in
      while !l <= !u do
        invariant { 0 <= !l /\ !u <= n-1 }
        invariant {
          forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
        variant { !u - !l }
        let m = div (!l + !u) 2 in
        if get_ t m < v then l := m + 1
        else if get_ t m > v then u := m - 1
        else raise (Return m)
      done;
      raise (Return (-1))
    with Return r ->
      r
    end
end

(* Finally, let us prove the absence of arithmetic overflow
*)

module M3

  use int.Int
  use int.ComputerDivision
  use ref.Ref

  type int32
  val function to_int int32 : int

  axiom int32_domain : forall x:int32. -2147483648 <= to_int x <= 2147483647

  val of_int (x:int) : int32
    requires { -2147483648 <= x <= 2147483647 }
    ensures  { to_int result = x }

  type pointer
  type memory
  function get memory pointer int : int32

  val mem : ref memory

  function block_size memory pointer : int

  val get_ (p:pointer) (ofs:int32) : int32
    requires { 0 <= to_int ofs < block_size !mem p }
    ensures  { result = get !mem p (to_int ofs) }

  exception Return int32

  let binary_search (t : pointer) (n : int32) (v : int32)
    requires { 0 <= to_int n <= block_size !mem t }
    requires { forall k1 k2:int.
        0 <= k1 <= k2 <= to_int n - 1 ->
        to_int (get !mem t k1) <= to_int (get !mem t k2) }
    ensures  { (to_int result >= 0 /\
       to_int (get !mem t (to_int result)) = to_int v)
      \/
      (to_int result = -1 /\
       forall k:int. 0<=k<to_int n -> to_int (get !mem t k) <> to_int v) }
  = try
      let l = ref (of_int 0) in
      let u = ref (of_int (to_int n - to_int (of_int 1))) in
      while to_int !l <= to_int !u do
        invariant { 0 <= to_int !l /\ to_int !u <= to_int n - 1 }
        invariant { forall k:int. 0 <= k < to_int n ->
          to_int (get !mem t k) = to_int v -> to_int !l <= k <= to_int !u }
        variant { to_int !u - to_int !l }
        let m = of_int (to_int !l
                        +
                        to_int
                          (of_int
                             (div (to_int (of_int (to_int !u - to_int !l)))
                                  (to_int (of_int 2)))))
        in
        if to_int (get_ t m) < to_int v then l := of_int (to_int m + 1)
        else if to_int (get_ t m) > to_int v then u := of_int (to_int m - 1)
        else raise (Return m)
      done;
      raise (Return (of_int (-1)))
    with Return r ->
      r
    end
end