STEP-BY-STEP LESSON · §5.5
Application: Correctness of Algorithms
Distinguish invariant preservation from algorithm termination.
Before you begin
Mathematical Induction I: Proving Formulas
P(n) must be a specific statement for every integer n in the stated range.
P(n): 1+2+…+n = n(n+1)/2, n≥1
Verify P(1) separately. Then choose arbitrary k≥1 and temporarily assume P(k).
1 = 1·2/2
Split the sum through k+1 into the known sum through k and the final term.
k(k+1)/2+(k+1)=(k+1)(k+2)/2
Application: Algorithms
Assignment evaluates the right side using current values and stores the result in the left variable. It changes the state.
x:=x+1
Sequential assignments use already updated values. Save an old value separately if it will be needed later.
r:=a mod b; a:=b; b:=r
Symbols
- I
- loop invariant
- :=
- assignment: replace the variable by the value on the right
Definitions and notation for this topic
Assignment and program state
x:=e
Evaluate e using the current variable values, then replace the value stored in x. A state records the current values of the algorithm’s variables.
The right-hand x is read before the replacement. Assignment is an action; x=4 is a statement about a state, and 4∈A is set membership.
Separate glossary example
Starting with x=3, the instruction x:=x+1 changes the state to x=4.
Loop invariant
A statement true whenever execution reaches a specified point of every loop iteration. Prove initialization and preservation; combine it with the exit condition.
At an exit with i=n, this gives the required sum. Proving an invariant alone does not prove termination; that requires a separate argument.
Separate glossary example
Before each iteration, s=1+…+i. Initially i=0,s=0. The updates i:=i+1; s:=s+i preserve this relation.
Step by step
Step 1 / 6
Separate the specification from the trace
The summation algorithm takes a fixed integer n≥0 and must return 1+…+n. At every loop test, require 0≤i≤n and s=i(i+1)/2. For n=0 the required sum is 0.
0≤i≤n ∧ s=i(i+1)/2
The invariant describes all iterations, while a trace describes only one input.
Worked example
Trace i=0,s=0; while i<3: i:=i+1; s:=s+i.
- After the first iteration i=1,s=1, the sum of processed numbers.
- After the second i=2,s=3=1+2; after the third i=3,s=6=1+2+3.
- The guard 3<3 is false. The invariant and i=3 explain why the result is the required sum.
Optional self-check
Replace the example’s guard i<3 with i<n. What does the algorithm return when n=0?
Show answer
0: the loop does not run, and the empty sum is 0.