examples/binary_search_vc_sp.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 Not_found (* raised to signal a search failure *)
  15
  16   let binary_search (a : array int) (v : int) : int
  17     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
  18     ensures  { 0 <= result < length a /\ a[result] = v }
  19     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  20   = [@vc:sp]
  21     let l = ref 0 in
  22     let u = ref (length a - 1) in
  23     while !l <= !u do
  24       invariant { 0 <= !l /\ !u < length a }
  25       invariant {
  26         forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
  27       variant { !u - !l }
  28       let m = !l + div (!u - !l) 2 in
  29       assert { !l <= m <= !u };
  30       if a[m] < v then
  31         l := m + 1
  32       else if a[m] > v then
  33         u := m - 1
  34       else
  35         return m
  36     done;
  37     raise Not_found
  38
  39 end
  40
  41 (* A generalization: the midpoint is computed by some abstract function.
  42    The only requirement is that it lies between l and u. *)
  43
  44 module BinarySearchAnyMidPoint
  45
  46   use int.Int
  47   use ref.Ref
  48   use array.Array
  49
  50   exception Not_found (* raised to signal a search failure *)
  51
  52   val midpoint (l:int) (u:int) : int
  53     requires { l <= u } ensures { l <= result <= u }
  54
  55   let binary_search (a :array int) (v : int) : int
  56     requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
  57     ensures  { 0 <= result < length a /\ a[result] = v }
  58     raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
  59   = [@vc:sp]
  60     let l = ref 0 in
  61     let u = ref (length a - 1) in
  62     while !l <= !u do
  63       invariant { 0 <= !l /\ !u < length a }
  64       invariant {
  65         forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
  66       variant { !u - !l }
  67       let m = midpoint !l !u in
  68       if a[m] < v then
  69         l := m + 1
  70       else if a[m] > v then
  71         u := m - 1
  72       else
  73         return m
  74     done;
  75     raise Not_found
  76
  77 end
  78
  79 (* binary search using 32-bit integers *)
  80
  81 module BinarySearchInt32
  82
  83   use int.Int
  84   use mach.int.Int32
  85   use ref.Ref
  86   use mach.array.Array32
  87
  88   (* the code and its specification *)
  89
  90   exception Not_found   (* raised to signal a search failure *)
  91
  92   let binary_search (a : array int32) (v : int32) : int32
  93     requires { forall i1 i2 : int. 0 <= i1 <= i2 < a.length ->
  94                a[i1] <= a[i2] }
  95     ensures  { 0 <= result < a.length /\ a[result] = v }
  96     raises   { Not_found ->
  97                  forall i:int. 0 <= i < a.length -> a[i] <> v }
  98   = [@vc:sp]
  99     let l = ref 0 in
 100     let u = ref (length a - 1) in
 101     while !l <= !u do
 102       invariant { 0 <= !l /\ !u < a.length }
 103       invariant { forall i : int. 0 <= i < a.length ->
 104                   a[i] = v -> !l <= i <= !u }
 105       variant   { !u - !l }
 106       let m = !l + (!u - !l) / 2 in
 107       assert { !l <= m <= !u };
 108       if a[m] < v then
 109         l := m + 1
 110       else if a[m] > v then
 111         u := m - 1
 112       else
 113         return m
 114     done;
 115     raise Not_found
 116
 117 end
 118
 119 (* A particular case with Boolean values (0 or 1) and a sentinel 1 at the end.
 120    We look for the first position containing a 1. *)
 121
 122 module BinarySearchBoolean
 123
 124   use int.Int
 125   use int.ComputerDivision
 126   use ref.Ref
 127   use array.Array
 128
 129   let binary_search (a: array int) : int
 130     requires { 0 < a.length }
 131     requires { forall i j. 0 <= i <= j < a.length -> 0 <= a[i] <= a[j] <= 1 }
 132     requires { a[a.length - 1] = 1 }
 133     ensures  { 0 <= result < a.length }
 134     ensures  { a[result] = 1 }
 135     ensures  { forall i. 0 <= i < result -> a[i] = 0 }
 136   = [@vc:sp]
 137     let lo = ref 0 in
 138     let hi = ref (length a - 1) in
 139     while !lo < !hi do
 140       invariant { 0 <= !lo <= !hi < a.length }
 141       invariant { a[!hi] = 1 }
 142       invariant { forall i. 0 <= i < !lo -> a[i] = 0 }
 143       variant   { !hi - !lo }
 144       let mid = !lo + div (!hi - !lo) 2 in
 145       if a[mid] = 1 then
 146         hi := mid
 147       else
 148         lo := mid + 1
 149     done;
 150     !lo
 151
 152 end