5 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 something

by edanm 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. A `for` (usually) means you're going to be looping over an array, with a specific length, with a specific "step" (usually one). This is information you immediately get by seeing a `for`. Moreover, you get all the information about how the loop looks (what you're looping over, size of the array, other actions you intend to perform in the loop) all in one place. This especially helps when you're looking at a large piece of code, in which case your example of "while (cond) {...;inc;}" would have a lot of lines between the condition and the increment.

RiderOfGiraffes 16y ago
But I observe that in C when iterating over a string you don't know in advance how big it is, you merely have to keep going until you find the '\0'. That's why some people will find it more natural to use a "while" when walking down a string.
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 ago
  I 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 ago
    I 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 ago
    You should write that up as a proper tutorial - I'm pretty sure a few people here would find it interesting.
    - smcl 16y ago
      Should I be concerned that I've never encountered these Hoare Triples before in my life?

by edanm 16y ago

RiderOfGiraffes 16y ago

But I observe that in C when iterating over a string you don't know in advance how big it is, you merely have to keep going until you find the '\0'. That's why some people will find it more natural to use a "while" when walking down a string.

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 ago
I 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 ago
  I 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 ago
  You should write that up as a proper tutorial - I'm pretty sure a few people here would find it interesting.
  - smcl 16y ago
    Should I be concerned that I've never encountered these Hoare Triples before in my life?