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.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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|cite|improve this question

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=1$, and the loop invariant is true.

share|cite|improve this answer
    
Why do we have i = 0 instead of i = 1 after the initialisation? – Musa Al-hassy Apr 7 at 18:19
    
That was an error; I change my mind about the loop bounds. Thanks for pointing this out. – Mark Dominus Apr 7 at 19:21

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.