Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

From CLRS (third edition, page 19), there is a footnote:

When the loop is a for loop, the moment at which we check the loop invariant just prior to the first iteration is immediately after the initial assignment to the loop-counter variable and just before the first test in the loop header.

Why is the checking moment specifically chosen to be after the initial assignment but before the first test? Note the excerpt is talking about proving correctness of algorithms using loop invariants.

share|improve this question
add comment

1 Answer 1

The loop invariant probably involves the loop control variable. If so, it only makes sense to ask if the invariant is true, when the loop control variable is initialized. When the loop control variable is uninitialized, expressions that involve it are undefined.

Consider a simple example, a loop whose purpose is to determine whether all the elements of a (0-based) array $a$ are equal:

   all_equal = true
   for (i = 1; i < a.size; i++)
      if a[i-1] ≠ a[i] 
         all_equal = false

Here the loop invariant is that $all\_equal$ is true if and only if the $a[k]$ are all equal for each $k$ with $0 \le k \le i$.

This is makes no sense at all unless the loop control variable $i$ has a well-defined value. Before the initialization, it doesn't. After the initialization, we have $i=0$, and the loop invariant is true.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.