Merge branch 'mailmap' into 'master'
[why3.git] / examples / binary_search_vc_sp.mlw
blobd5a06e57e036083b7eeabf7bfa6eb98c91393b5d
1 (* Binary search
3    A classical example. Searches a sorted array for a given value v. *)
5 module BinarySearch
7   use int.Int
8   use int.ComputerDivision
9   use ref.Ref
10   use array.Array
12   (* the code and its specification *)
14   exception Not_found (* raised to signal a search failure *)
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
39 end
41 (* A generalization: the midpoint is computed by some abstract function.
42    The only requirement is that it lies between l and u. *)
44 module BinarySearchAnyMidPoint
46   use int.Int
47   use ref.Ref
48   use array.Array
50   exception Not_found (* raised to signal a search failure *)
52   val midpoint (l:int) (u:int) : int
53     requires { l <= u } ensures { l <= result <= u }
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
77 end
79 (* binary search using 32-bit integers *)
81 module BinarySearchInt32
83   use int.Int
84   use mach.int.Int32
85   use ref.Ref
86   use mach.array.Array32
88   (* the code and its specification *)
90   exception Not_found   (* raised to signal a search failure *)
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
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. *)
122 module BinarySearchBoolean
124   use int.Int
125   use int.ComputerDivision
126   use ref.Ref
127   use array.Array
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