### 5. Consider the following program segment:
```text
i := 1
total := 1
while i < n do
i := i + 1
total := total + i
````
Let
( p ) be the proposition:
[
p:\quad ( \text{total} = \frac{i(i+1)}{2} \ \text{and}\ i \le n )
]
Use mathematical induction to prove ( p ) is a loop invariant.
---
## Solution
### Basis Step
Before the loop is entered, ( p ) is true since
[
\text{total} = 1 = \frac{1(1+1)}{2}
]
and
[
i \le n
]
---
### Inductive Step
Suppose ( p ) is true and ( i = k < n ) after the ( k - 1 )-th execution of the loop.
Since ( p ) is true:
[
\text{total} = \frac{k(k+1)}{2}
]
Suppose that the while loop is executed again. Then ( i ) is incremented to
[
i = k + 1
]
Total becomes:
[
\begin{aligned}
\text{total}
&= \text{total}_{\text{prev}} + i \
&= \frac{k(k+1)}{2} + (k+1) \quad \text{(by inductive hypothesis)} \
&= \frac{k(k+1) + 2(k+1)}{2} \
&= \frac{(k+1)(k+2)}{2}
\end{aligned}
]
---
After the loop, ( i \le n ) and `total` is still of the required form.
Therefore, ( p ) is a loop invariant. ∎