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

 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?
 Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.
 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/2142. 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!
 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.
 > Can something like that work?Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works.Therefore, I hereby declare that you are ready to use and learn more about Why3/WhyML.Here's a working complete implementation of your version: https://clbin.com/cwvKYThere's only a minor caveat with your version: there's no formal guarantee that `binary_search` won't call `pred` below `low` or above `high`, because (as far as I know) we can't encode those requirements if we pass the function as an argument. Maybe there's a way to do that, but I don't know WhyML that deeply.> Those tests are only necessary for the proofs, right?I think so. We can probably separate `pred` into a logical version and a run-time version, making sure that the result of the logical `pred` matches the result of the run-time `pred` when `-1 < idx < length arr`.I think this should be very easy to do with WhyML, I will try and figure out if I can do it.
 That would be nice, then the run time predicate can be fast while the logical version remains elegant.What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually. That property ensures that the answer will be unique, but the algorithm will find a point pred i = False /\ pred (i+1) = True even if the predicate does not satisfy that property.If you add the uniqueness to the ensures, does Z3 still automatically prove it correct?`` ensures { forall j. pred j = False /\ pred (j+1) = True -> j == result) }``
 > What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually.If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_search` automatically anymore (using the Z3, CVC4 and Eprover automatic provers that I have installed).Specifically, Why3 tries to split the postcondition into the 2 parts: `pred result = False`, which gets verified correctly, and `pred (result+1) = True`, which cannot be verified automatically.I think this is because nothing stops `high` from actually being lower than `low`. If someone passes those 2 arguments reversed (high as low and low as high), then probably the algorithm wouldn't work, right? At least, Why3 is not convinced that it would work.However, if I add this loop invariant: `!cur_low < !cur_high` and this function precondition: `requires { low < high }`, then it all works fine! (both are required).Diff here: https://clbin.com/wVkhO And full code here: https://clbin.com/2gBfJI tried separating `pred` into logical and run-time versions (one with the ifs and the other only with the comparison), and it all seems to work fine, except for one problem:The run-time version of `pred` is a partial function (it only works for valid array indices), so it needs a precondition. However, when I pass `pred` as an argument to `binary_search`, I can't / don't know how to specify that the argument needs the precondition.Therefore, Why3 complains that the precondition of `pred` may not be respected (all other verification conditions are proven to be valid).I could do what I did before (making `low` and `high` functions, etc) but that greatly complicates the code...Maybe there is some way to do that, but currently I don't know how.
 > I think this is because nothing stops `high` from actually being lower than `low`.Ahh, right. I guess that's exactly the type of oversight that a checker is for :)We could return the pair (!cur_low, !cur_high) and have the postcondition that pred (fst result) = False and pred (snd result) = True and abs (first result - snd result) = 1. Then it would work also if low > high, but I'm not sure this is useful in practice...> The run-time version of `pred` is a partial function (it only works for valid array indices), so it needs a precondition. However, when I pass `pred` as an argument to `binary_search`, I can't / don't know how to specify that the argument needs the precondition.If I'm understanding this correctly, you want to do something like this:`````` let binary_search (pred: (i:int) -> bool requires { low < i < high }) (low: int) (high: int): int `````` But Why3 does not support this?If you add a precondition like that to pred, wouldn't that also prevent requires/ensures/invariant from calling pred on arguments that don't satisfy the precondition? In the precondition we do want pred low = False /\ pred high = True, but the run time predicate only allows pred k for low < k < high?