3 ms·
I think both for sum and max a better invariant should include the uncalculated part. Sum(0..X)=Sum(0..i)+sum(i+1..X) with the moving i. So it is true at first
by maweki 8y ago
I think both for sum and max a better invariant should include the uncalculated part.
Sum(0..X)=Sum(0..i)+sum(i+1..X) with the moving i. So it is true at first because the unsummed part is empty and the missing part is the goal.
Then we take away an i from the solution to-go pile and put it on the done pile and when the loop has done X the to-do pile is enpty and per invariant the done pile equals the goal.
Including the goal in the invariant sometimes gives you nicer properties. The equivalence relation often also implies an algorithm.
For max I would say the equivalence is: Max(0..X)=Max(Max(0..I),max(I+1..X))
This of course only easier if the max of empty is negative infinity.
Then you can move the i from 0 to X.
- jonsen 8y agoYou 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.