[wizzwizz4]

Turn your first paragraph on its head:

Appropriate abstractions (i.e., "idiomatic code for the language and codebase") make program verification easy. If you are hand-weaving an appropriately-abstracted program, there's little benefit to thinking about loop invariants and pre-post conditions, since they don't exist at that level of generality: correct proofs follow directly from correct code.

[gregorygoc]

No, appropriate abstractions are insufficient for my argument. For example: there’s one way to write an idiomatic loop in C and it inherits necessary invariants by construction.

I highly recommend reading the book, it explains concept of writing idiomatic code way better than I ever could.

[chowells]

That's a really funny example, given how many bugs have been found in C programs because idiomatic loops are wrong in the edge cases.

How do you idiomatically write a loop to iterate over signed ints from i to j (inclusive) in increasing order, given i <= j?

What does that loop do when j is INT_MAX?

[wk_end]

I can imagine someone who sketches out little proofs in their head - or even on paper - missing that case too. It’s easy to forget you’re not doing normal arithmetic when doing arithmetic in C!

[chowells]

Yeah, it's a hard case in general. But C's idioms really don't encourage you to think about it. You really need to default to a loop structure that checks the termination condition after the loop body but before the increment operation for inclusive end coordinates.

It's easy to think that's what do/while is for, but it turns out to be really hard to do the increment operation after the conditional, in general. What you really want is a loop structure with the conditional in the middle, and the only general purpose tool you get for that is a break. C (or any language with similar syntax) really doesn't have an idiom for doing this correctly.

[wizzwizz4]

This may be hubris, but…

  int i = start;
  do thing_with(i) while (i++ <= end);

[chowells]

I did consider that, but I wrote "in general" for a reason. It works very specifically in the case of "add one" or "subtract one", but it doesn't work with anything more complicated, like chasing pointers or adding/subtracting more than one at a time.

You could write functions to do the update and return the old value so you could use them in the same way, but I don't like this either. This is mostly because it orders the termination check and the update logic the wrong way around. If there's IO involved in checking for the next thing, for example, side effects of that unnecessary operation might interfere with other code.

You could resolve that by moving the termination check into the update logic as well, but now you're seriously complecting what should be independent operations. I don't think the tradeoff is there versus just using a break. But mostly, this is a self-inflicted problem in C's language constructs and idioms. I just don't have this problem in many other languages, because they provide end-inclusive looping constructs.

[Izkata]

Isn't i going to be one past end on the last iteration?

I think you want either "++i <= end" or "i++ < end", and that's assuming "end" is inclusive. If it's exclusive then "++i < end", right?

(Using "<=" in a termination condition has become a code smell for me, it's been wrong more often than not, so it sticks out as "pay close attention here")