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.
--
Steve
_______________________________________________
Python-ideas mailing list
Python-ideas@python.org
https://mail.python.org/mailman/listinfo/python-ideas
Code of Conduct: http://python.org/psf/codeofconduct/
