> 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/wi

> 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.