5 ms·

Actually, I can definitely say that this version is not broken, i.e. I've formally proven it to be mathematically correct assuming that: 1. high and low are bi

Actually, I can definitely say that this version is not broken, i.e. I've formally proven it to be mathematically correct assuming that: 1. high and low are bigints (such as when using Python, for example) 2. the input array is sorted (needed for any binary search algorithm) 3. this missing code at the bottom is added: if (0 <= low && low < arr.length) { if (arr[low] == x) { return low; } } return -1; // (or "raise Not_found" or whatever you use to indicate that 'x' was not found). You can find the formal proof in WhyML below. This includes proofs that: 1. all array accesses are in bounds [checked automatically] 2. there is no undefined behavior (such as division by zero) [checked automatically] 3. the function always terminates [enforced automatically, proven with the help of the 'variant' clause] 4. there are no overflows [checked automatically, not possible since we're using bigints] 5. if an index is returned, the array has an element with value equal to x at that index [the 'ensures' clause] 6. if instead the function returns "not found", the array does not have any element with a value equal to x [the 'raises' clause] ... all this assuming that the input array is sorted [the 'requires' clause] Code + proof here (it makes more sense if you can read OCaml syntax): https://clbin.com/jbTk8 https://clbin.com/jbTk8

jules 8y ago
Awesome! Interesting that it can prove that given only the loop invariant. The inner loop could be factored to a subroutine with the following contract: let P be a predicate on the integers such that (i <= j) => (P(i) => P(j)), and let low be such that P(low) = false and high such that P(high) = true. The subroutine returns i such that P(i) = false and P(i+1) = true. The subroutine further promises to only call P(k) on low < k < high. This may be applied to the predicate P(k) = (x <= arr[k]) on the range (low,high) = (-1,arr.length) to find the point at which the predicate flips from false to true (we're essentially pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length], and the subroutine promises to only call P(k) on values strictly between -1 and arr.length). Is it possible to do this with WhyML?
- wizeman 8y ago
  Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3 https://clbin.com/OhyJ3 Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.
- wizeman 8y ago
  Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor caveats: 1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the following bug in Why3 (it's already fixed in the master branch, but not in the most recent release): https://gitlab.inria.fr/why3/why3/issues/214 https://gitlab.inria.fr/why3/why3/issues/214 2. It turns out that the value of "high" is not statically known at compile time, because it depends on the size of the array. So I changed "high" to be a function of the array rather than a constant (I did the same to "low" for consistency). 3. Similarly and consequently, the predicate P(i) is not only a function of "i". It's also a function of the value being searched for ("x"), i.e. if P(i) is true or not depends on which value you're searching for. This also means that P() is also a function of the specific array being searched for (because some arrays may have "x" but others not). 4. You said that "we're pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length]", but unless I misunderstood something, we can't actually pretend that, this must be written in the code somewhere, otherwise it won't work. For simplicity, I have chosen to implement those rules in the predicate itself. However, this is also enforced by the function with the while loop, i.e., it always makes sure that whatever predicate you have chosen, it has to implement those rules. I am sure that this could be changed, but I think it would complicate the proofs. The result is that in module "GenericBinarySearch", like the name says, we have a neat generic binary search function which works with any predicate P (called "pred" in the code), any function "low", any function "high" and for any type. And in module "ArrayBinarySearch" we have an instantiation of "GenericBinarySearch" which works for sorted arrays! Also note that the axiom in the code is only an axiom in the generic module (it specifies what must be true of P()), but when the generic module is instantiated, Why3 verifies that the axiom is actually true for the specific instance of the predicate (so there is no cheating). You can find the code in the link below. Enjoy! https://clbin.com/Ov3NX https://clbin.com/Ov3NX
  - jules 8y ago
    Very nice. I don't quite understand why you need the option in GenericBinarySearch. Doesn't the function always return Some? I had something like this in mind: let binary_search (pred: int -> bool) (low: int) (high: int): int requires { pred low = False } requires { pred high = True } requires { forall i j. (i <= j) -> (pred i -> pred j)} ensures { pred result = False /\ pred (result+1) = True } = let cur_low = ref low in let cur_high = ref high in while !cur_high - !cur_low > 1 do variant { !cur_high - !cur_low } invariant { pred !cur_low = False /\ pred !cur_high = True } let mid = div (!cur_high + !cur_low) 2 in if not (pred mid) then cur_low := mid else cur_high := mid done; !cur_low Can something like that work? let predicate pred (i: int) (x: t) (k: int) = if i <= low x then false else if i >= high x then true else k <= x.arr[i] Those tests are only necessary for the proofs, right? At run time the predicate will never be called with i <= low or i >= high, but only on low < i < high, because if high - low > 1 then low < (high + low)/2 < high. That's what I meant by pretending that the predicate returns false/true on -1 or arr.length: we don't actually need the predicate to work on those indices, because we never call the predicate at those indices.
karakot 8y ago
thanks, this is a great comment(and the rest of the thread). Yes, I meant that it doesn't work without assuming #1, and it had missing #3.

jules 8y ago

Awesome! Interesting that it can prove that given only the loop invariant. The inner loop could be factored to a subroutine with the following contract: let P be a predicate on the integers such that (i <= j) => (P(i) => P(j)), and let low be such that P(low) = false and high such that P(high) = true. The subroutine returns i such that P(i) = false and P(i+1) = true. The subroutine further promises to only call P(k) on low < k < high. This may be applied to the predicate P(k) = (x <= arr[k]) on the range (low,high) = (-1,arr.length) to find the point at which the predicate flips from false to true (we're essentially pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length], and the subroutine promises to only call P(k) on values strictly between -1 and arr.length). Is it possible to do this with WhyML?

wizeman 8y ago
Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3 https://clbin.com/OhyJ3 Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.
wizeman 8y ago
Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor caveats: 1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the following bug in Why3 (it's already fixed in the master branch, but not in the most recent release): https://gitlab.inria.fr/why3/why3/issues/214 https://gitlab.inria.fr/why3/why3/issues/214 2. It turns out that the value of "high" is not statically known at compile time, because it depends on the size of the array. So I changed "high" to be a function of the array rather than a constant (I did the same to "low" for consistency). 3. Similarly and consequently, the predicate P(i) is not only a function of "i". It's also a function of the value being searched for ("x"), i.e. if P(i) is true or not depends on which value you're searching for. This also means that P() is also a function of the specific array being searched for (because some arrays may have "x" but others not). 4. You said that "we're pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length]", but unless I misunderstood something, we can't actually pretend that, this must be written in the code somewhere, otherwise it won't work. For simplicity, I have chosen to implement those rules in the predicate itself. However, this is also enforced by the function with the while loop, i.e., it always makes sure that whatever predicate you have chosen, it has to implement those rules. I am sure that this could be changed, but I think it would complicate the proofs. The result is that in module "GenericBinarySearch", like the name says, we have a neat generic binary search function which works with any predicate P (called "pred" in the code), any function "low", any function "high" and for any type. And in module "ArrayBinarySearch" we have an instantiation of "GenericBinarySearch" which works for sorted arrays! Also note that the axiom in the code is only an axiom in the generic module (it specifies what must be true of P()), but when the generic module is instantiated, Why3 verifies that the axiom is actually true for the specific instance of the predicate (so there is no cheating). You can find the code in the link below. Enjoy! https://clbin.com/Ov3NX https://clbin.com/Ov3NX
- jules 8y ago
  Very nice. I don't quite understand why you need the option in GenericBinarySearch. Doesn't the function always return Some? I had something like this in mind: let binary_search (pred: int -> bool) (low: int) (high: int): int requires { pred low = False } requires { pred high = True } requires { forall i j. (i <= j) -> (pred i -> pred j)} ensures { pred result = False /\ pred (result+1) = True } = let cur_low = ref low in let cur_high = ref high in while !cur_high - !cur_low > 1 do variant { !cur_high - !cur_low } invariant { pred !cur_low = False /\ pred !cur_high = True } let mid = div (!cur_high + !cur_low) 2 in if not (pred mid) then cur_low := mid else cur_high := mid done; !cur_low Can something like that work? let predicate pred (i: int) (x: t) (k: int) = if i <= low x then false else if i >= high x then true else k <= x.arr[i] Those tests are only necessary for the proofs, right? At run time the predicate will never be called with i <= low or i >= high, but only on low < i < high, because if high - low > 1 then low < (high + low)/2 < high. That's what I meant by pretending that the predicate returns false/true on -1 or arr.length: we don't actually need the predicate to work on those indices, because we never call the predicate at those indices.

karakot 8y ago

thanks, this is a great comment(and the rest of the thread). Yes, I meant that it doesn't work without assuming #1, and it had missing #3.