Loop invariant for a binary search

[bearophile]

Lutger:

> What do you think about expressing the loop invariant as as nested pure 
> function?

It's good enough to satisfy the basic 'requirements' I have listed for a invariant syntax :-)
Thank you for the idea.

That D code that tests the invariant is long. This was part of the invariant in Eiffel that translated to D requires some lines:
forall k : rowList @ row .. pp :: k.column < column

>From what I have seen so far contracts are a place where language conciseness is really important. Because they must be correct, use short space, they are almost mathematical in their nature. Some of the "micropatterns" Andrei has put in std.range can help a bit here (to shorten the code inside contracts), I will probably give more micropatterns to Andrei to add them to std.range. I can't believe how only few languages like Lisp and Python seem to have understood how fundamental micropatterns are in programming.

Bye,
bearophile