induction variable optimization

[mccaugh at uiucdcsm.UUCP]

 Yes, the two fragments of code are semantically equivalent in that they
 should yield as final value j(final) = j(initial) + 315. Of course, if
 j(initial) = undefined, they will still be equivalent!
 A loop-invariant for the first fragment is: 
       (i=#) & (j(#) = j(initial) + 7*(1 + ... + #-1))
 where '#' = number of cycles (of the FOR-loop); a loop-invariant for the
 second fragment is similar: (i=7*#) & (j(#) = j(initial) + 7*(1 + ... + #-1)).
 Both fragments will cycle 10 times, so that:
     j(final) = j(10) = j(initial) + 7*(9*10)/2 
              = j(initial) + 315.

 (But the final values of i of course differ: i(final) = 10 in the first
  fragment, and 70 in the second -- I here assumed that 'i' was a loop-
  counter and that 'j' was the variable of interest.)

 The efficiency gained in the second fragment is to replace a multiplication
 by an addition, considered "efficient" since the simplification is repeated
 ten times.

 I apologize for this verbose response, which I only entered after reading the
 first 5 and being disappointed to find no demonstration of the equivalence
 claimed for the 2 fragments. (I sincerely hope this fills that gap.)

 -- Scott McCaughrin (mccaugh at uiucmsl)