On a slightly related note… Competitive programming is surprisingly good at teaching you the right set of techniques to make sure your code is correct. You won’t progress beyond certain stage unless you pick them up.
On a slightly related note… Competitive programming is surprisingly good at teaching you the right set of techniques to make sure your code is correct. You won’t progress beyond certain stage unless you pick them up.
Code for which there is not even a toehold for an imagined proof might be worth cordoning off from better code.
The answer is yes, both words are related to idios, "own", "self", "private".
To give a more concrete example: I have recently seen a very complicated piece of logic checking whether a subsequent code should be even invoked, but it was hidden in a debris of core logic and other verification. It easily could have been separated and rewritten as a series of early returns and this is what a precondition is. I’m sure someone who wrote the code had it in their mind but was not familiar enough with the early return technique to embed this in code. Had they been, their brain power could’ve been utilized more efficiently.
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.
I highly recommend reading the book, it explains concept of writing idiomatic code way better than I ever could.
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?
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.
int i = start;
do thing_with(i) while (i++ <= end);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.
You're reminding me of the book "Modern Compiler Design." The author goes over how to compile a general Pascal-style for-loop correctly, accounting for increasing or decreasing ranges, differing step sizes, and accounting for overflow. It was written using just goto statements, so I adapted a version of it to C. Just replace "intN_t" with an actual integer size. It works by calculating the number of times the loop will run. If "from" is equal to "to," it's still going to run at least once. Again, this is not mine, just adapted from the author's code (Dick Grune's).
// enumerate: print out numbers from "from" to "to", inclusive, with step size "by"
void enumerate(intN_t from, intN_t to, intN_t by) {
uintN_t loop_count;
intN_t i;
if (by > 0) {
if (from > to) return;
loop_count = (to - from) / by + 1;
} else if (by < 0) {
if (from < to) return;
loop_count = (from - to) / -by + 1;
} else /* (by == 0) */ {
// Maybe some kind of error
return;
}
for (i = from; ; i += by) {
printf("%d\n", i);
if (--loop_count == 0) break;
}
}
You can see it's more complicated than the idiomatic C for-loop, haha. But that's just a general solution. Like you guys noted, it could be simpler for step sizes of 1.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")
Edit: Just checked in with a C expert. The UB is in the increment operation, so that's not correct after all. You really do just need to separate out the update from the test entirely.
assert(i <= j);
for (;;) {
do_something_with(i);
if (i == j)
break;
i++;
}But writing clean and clear code in the hopes that it's good aesthetics will result in correctness would be cargo culting. (Writing clean code is still worthwhile of course, and clean code + code review is likely to result in better correctness.)
Form follows function, not the other way around.