> 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?