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.
Obviously the loop invariant has to be attached to the loop. You can't attach a loop invariant to a method or class, because they might contain more than one loop.
That's not so obvious. At least in theory you could provide a label for the loop (Common Lisp for example has named blocks), and refer to that in an "invariant" section outside the function. I couldn't imagine a pleasing syntax without help from someone who's used contracts, though. That's why I asked. It's not a big deal that they aren't both simultaneously true in practice, it's just that there are a huge number of abstract claims being made for contracts, and for my money they don't look anywhere near as much of an improvement over asserts in practice as they sound in the abstract, in decorator form or in Eiffel syntax. As I said before, since a number of people are asking for them, I'm at least +0 on including a contracts module with attractive syntax for contracts in the stdlib on the general principle that we should provide batteries for as many common patterns or styles as possible. But I'm not ready to go that high for language changes for this purpose, at least not yet. Since I don't expect to be using contracts any time soon, I'll leave the definition of "attractive" up to those who expect to have to read them frequently. Steve