On Tue, Oct 02, 2018 at 02:43:57AM +0900, Stephen J. Turnbull wrote:
Steven D'Aprano writes:
I'm not sure how Stephen went from my comment that you can't unit test loop invariants to the idea that loop invariants aren't in the implementation.
Obviously I didn't. I went from your statement that (1) contracts are separated from the implementation and the inference from (7) that contracts can specify loop invariants to the question of whether both can be true at the same time.
Okay, fair enough.
The loop invariant is separate in the sense that it is in a distinctly named block. But it connected in the sense that the loop invariant is attached to the loop, which is inside the function implementation, rather than in a separate block outside of the implementation.
In Python terms, we might say something like:
for x in sequence: BLOCK else: BLOCK invariant: BLOCK
Static tools could parse the source and extract the invariant blocks, editors could allow you to collapse them out of sight. But unlike the (hypothetical) require and ensure blocks, its right there inside the function implementation.
We presumably wouldn't want the invariant to be far away from the loop:
... code ... more code for x in sequence: BLOCK ... more code ... more code ... # and far, far away invariant: BLOCK
Even if we had some mechanism to connect the two (some sort of label, as you suggest) it would suck from a readability perspective to have to jump backwards and forwards from the loop to the loop invariant.
Things which are closely connected ought to be close together.