3 ms·
> I think for loops are better than while loops for looping over arrays. I'll try and explain my reasoning: > Whenever you see a `for` loop, it tells you someth
by jemfinch 16y ago
> I think for loops are better than while loops for looping over arrays. I'll try and explain my reasoning:
> Whenever you see a `for` loop, it tells you something that a `while` loop doesn't. It tells you the kind of loop you're about to do.
I won't disagree with that in theory, but I don't really think the "for" loop is the solution. The real solution, I think, is a "foreach" construct (whether it's a loop built into the language (á la Java/C#) or a higher-order function (á la C++'s std::for_each), I don't really care) for iterating over arrays and other collections.
In practice, I think the for loop is too often abused for too little gain, and I think C would be a better language without it.
As an aside, I wonder if anyone has provided a suitable Hoare triple for C's for loop. I have an idea of what it would look like, but would love to see someone else's efforts to verify my own internalized one.
- edanm 16y agoI love higher language's foreach construct. Have to work with what we've got though, and in C, the `for` loop is it. By the way, I don't know what a Hoare triple is, and reading a little on Wikipedia didn't enlighten me. Any chance for an explanation?
- jemfinch 16y agoI assume you read http://en.wikipedia.org/wiki/Hoare_logic http://en.wikipedia.org/wiki/Hoare_logic ? Basically, the (relevant) state of the computation is represented as a set of logical propositions which are true before a statement, and a set of logical propositions which are true after the statement. For each kind of statement the language supports (`if` statements, `while` statements, etc.) there are natural ways to reason about those triples. Do you understand the "While rule" on the link above? I can explain it in natural language, but I'd rather not expend the effort if it's not something you've already seen.
- gjm11 16y ago> I wonder if anyone has provided a suitable Hoare triple for C's for loop. Basically the same as for a while loop, as given e.g. at http://en.wikipedia.org/wiki/Hoare_logic http://en.wikipedia.org/wiki/Hoare_logic since (apart from the behaviour of continue) for (inits; cond; steps) { body } and inits; while (cond) { body; steps } are equivalent. And if you do want to deal with continue (and presumably also break) the Hoare stuff gets awfully cumbersome; you're probably better off using informal correctness proofs and writing down a lot of loop invariants. Oh, all right, here's how you do it. Suppose you have the following three Hoare triples. {P & Q0 & !cond} body; steps {P & body never invoked break or continue} {P & Q1 & !cond} body {P & body invoked continue} {P & Q2 & !cond} body {R & body invoked break} where Q0, Q1, Q2 are mutually exhaustive (but not necessarily mutually exclusive). And suppose you have {P0} inits; {P} Then you have {P0} for (inits; cond; steps) body {R | (P & !cond)} That's if you adopt the convention that any precondition is valid for code that doesn't terminate. Otherwise, you need to do some stuff with loop variants. for (char * rd=str; *rd; ++rd) { if (*rd != remove) *str++ = *rd; } *str = '\0'; We can take P0: str points to a zero-terminated string. P: so does rd, rd and str point to tails of the original string, rd >= str, and what's between original_str and str consists of an appropriately crunched version of what was originally between original_str and rd. Q0,Q1,Q2: true,false,false. R: not needed. We deduce that at the end of the for loop, rd points to a tail of the original string (P), it also points to a zero character (!cond), hence it points to the end of the original string. Hence what's between original_str and str consists of an appropriately crunched version of the entire original string. Hence all we need do is put on the final zero character, and we're finished.
- RiderOfGiraffes 16y agoYou should write that up as a proper tutorial - I'm pretty sure a few people here would find it interesting.
- smcl 16y agoShould I be concerned that I've never encountered these Hoare Triples before in my life?