[Python-ideas] Simplicity of C (was why is design-by-contracts not widely)

Steven D'Aprano steve at pearwood.info
Mon Oct 1 21:23:31 EDT 2018

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:

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:
... more code
... more code
# and far, far away

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.


More information about the Python-ideas mailing list