4 ms·
You are merging the invariant with the variant. The loop invariant is supposed to tell about the state of the variant at any loop start. The variant in this cas
by jonsen 8y ago
You are merging the invariant with the variant.
The loop invariant is supposed to tell about the state of the variant at any loop start.
The variant in this case is the tupple (i,sum).
Your version does not say anything about the stepwise evaluation of the sum.
- maweki 8y agoOf course this tells me about the state of the variant. And it's the same invariant the author uses but with the equation balanced differently. The author's invariant is Sum = 1+2+..I Mine is Sum+(I+1)+...+X = 1+2+..I+(I+1)+...+X That's both fine and tells us about I. I think the version that contains the value we want to obtain is easier to prove correctness for.