= Summation loop verification
{title2=$2s=n(n+1)$}
Compute $1+2+\cdots+n$, the <triangular number> $T_n$, for a nonnegative <integer> $n$. The <empty sum> gives zero when $n=0$. Use exact mathematical <integers> and keep the <input> $n$ unchanged; every comparison and <variable assignment> is a terminating operation. The original sequential procedure is
``
require n is an integer and n >= 0
i = 0
s = 0
while i < n:
i = i + 1
s = s + i
return s
``
The order of the two <variable assignments> matters: the <addition> uses the newly incremented $i$. For $n=4$, the pairs $(i,s)$ at successive condition checks are $(0,0),(1,1),(2,3),(3,6),(4,10)$. At the last check, $i<n$ is false, and the returned <sum> is $10$.
The <precondition> is $n\in\mathbb Z$ with $n\geq0$, under the exact-arithmetic model just stated. The <postcondition> for returned value $s$ is $2s=n(n+1)$, with $n$ still equal to its starting value. At each condition check use the <loop invariant>
$$
I:\qquad i,s\in\mathbb Z,\qquad 0\leq i\leq n,\qquad 2s=i(i+1),
$$
and the <loop variant> $V=n-i$. The equation says that the accumulator is the <triangular number> for precisely the processed prefix $1,\ldots,i$; the inequalities connect that prefix to the loop's condition.
\Image[/summation-loop-contract-control-flow.png]
{title=The summation loop restores its invariant before each condition check}
{description=Original sequential control flow for the <summation loop verification>. The blue loop head carries the <loop invariant>; the orange body increments $i$ before adding it to $s$. A false condition leads to the <postcondition>. The <loop variant> decreases on the return arrow. All values are mathematical <integers> and $n$ remains unchanged.}
Initialization gives $i=s=0$, so $I$ holds, including when $n=0$. For preservation, let the old values satisfy $I$ and $i<n$. Write $i'=i+1$ and $s'=s+i'$ for the values after both <variable assignments>. Since $i,n$ are <integers>, $i<n$ gives $i'\leq n$, and
$$
2s'=2s+2(i+1)=i(i+1)+2(i+1)=(i+1)(i+2)=i'(i'+1).
$$
Thus the completed body restores $I$. Between the two <variable assignments>, the equation can be false; the <loop invariant> is required at the loop head. This preservation step is <mathematical induction> on the number of completed iterations.
At exit, the false condition gives $i\geq n$, while $I$ gives $i\leq n$. Hence $i=n$, so $2s=n(n+1)$: this proves <partial correctness>. For <algorithm termination>, $I$ gives the nonnegative <integer> $V=n-i$. When the condition is true, $V\geq1$; the terminating body gives $V'=n-i'=V-1$. Therefore the loop cannot repeat forever. Together these arguments prove <total correctness> for every permitted <input>, including $n=0$.
\Image[/summation-loop-trace-and-stalled-variant.png]
{title=Four additions finish the sum; an unchanged index cannot make progress}
{description=Original exact trace for $n=4$: five condition checks and four body executions give $s=10$, while the <loop variant> decreases from four to zero. The right panel shows the stalled loop from <partial correctness>: the same <program state> repeats and $V=4$ never decreases. Its equation $2s=i(i+1)$ remains true, but it never reaches an exit.}
Two changes expose what the proof checks. Swapping the two body instructions computes $0+1+\cdots+(n-1)$, returning $6$ rather than $10$ for $n=4$. Leaving $i$ unchanged can preserve an initial equation forever without producing any answer. The first change breaks the intended <postcondition>; the second breaks <algorithm termination>. A trace can reveal these failures, while the two proof obligations explain them.
The exact-arithmetic assumption has a concrete boundary. In a stipulated unsigned eight-<bit> model where each <addition> wraps modulo $256$, $n=23$ fits in the <input> representation, but its intended <triangular number> is $276$. The stored accumulator instead finishes at $20$, so the mathematical <postcondition> fails. This is <integer overflow>, and the proof above does not apply to that altered model. Restricting the same implementation to $0\leq n\leq22$ prevents overflow in its stored loop values, since $T_{22}=253$; alternatively use a representation supporting the required exact <integer arithmetic>. The equations in the proof are mathematical statements, not instructions to evaluate products in eight <bits>.
Back to article page
