Algorithms & Data Structures – Correctness of Algorithms

1. Algorithm – Basic Notion

Etymology & informal meaning
- From the name of Persian‐Arab mathematician al-Khwārizmī.
- Stands for a finite, well–defined, effective procedure that transforms input data into output data.
Formal characteristics
- Finiteness – terminates after a finite number of steps.
- Definiteness – every instruction is precisely stated; no ambiguity.
- Input – zero or more quantities supplied externally.
- Output – at least one result produced.
- Effectiveness – each instruction can be carried out mechanically in finite time.

Specification: What the algorithm is required to accomplish.
- Expressed as pre-condition \text{Pre}(I) and post-condition \text{Post}(O).
Implementation: The concrete sequence of instructions.
Correctness question: \forall\,\text{valid } I\;(\text{Algorithm}(I) = O \land \text{Post}(O)) provided \text{Pre}(I).

Partial correctness
- If the algorithm terminates then the post-condition is true.
- Formally: \text{Pre} \land \text{Terminates} \;\Rightarrow\; \text{Post}.
Total correctness
- Partial correctness + proof of termination.
- Formally: \text{Pre} \;\Rightarrow\; (\text{Terminates} \land \text{Post}).

Mathematical induction – often the backbone.
Loop invariants – central pattern for iterative programs.
1. Initialization: invariant true before first iteration.
2. Maintenance: if invariant true before an iteration, remains true after executing the body.
3. Termination: when loop finishes, invariant + exit condition ⇒ post-condition.
Well-ordering principle / Variant function – to show termination by attaching a non-negative integer measure that strictly decreases.
Structural induction – for recursive algorithms (mirrors call tree).

Input: array A[0..n-1] and a candidate value x.
Goal / Post-condition
- \bigl(\forall\,0 \le j < n\; :\; x \ge A[j]\bigr) \land \bigl(\exists\,0 \le j < n\; :\; x = A[j]\bigr)
- “x is at least as large as every element and appears in the array.”
Naïve algorithm (pseudocode)

found ← false
for j ← 0 .. n-1 do
    if A[j] >  x then STOP with ‘not maximum’
    if A[j] == x then found ← true
end for
return found

Loop invariant after processing the prefix A[0..k-1] (index k about to be processed):
- \bigl(\forall\,0 \le j < k : x \ge A[j]\bigr) \land (found = \exists\,0 \le j < k : x = A[j])
Proof sketch
- Init k=0: vacuously true.
- Maint: examine A[k], update found, if A[k] > x halt (partial-correct). Otherwise invariant preserved.
- Term k=n ⇒ invariant yields post-condition; if halted early, post-condition violated ⇒ correct negative answer.
Termination measure: n-k decreases by 1 each iteration.

Base cases satisfy post-conditions directly.
Induction hypothesis acts on smaller parameters.
Induction step must combine recursive calls to produce overall post-condition.
Example pattern: MergeSort
- Pre: arbitrary array.
- Post: sorted permutation.
- Proof uses induction on array length.

Implication chains
- \text{Invariant} \land \neg\text{Cond}\;\Rightarrow\; \text{Post}
Existential–universal split
- Show existence once, then maintain universality.
Conjunctive decomposition
- Prove each conjunct of post-condition separately, often with the same invariant.

Ranking / variant functions V : \text{State} \to \mathbb{N} such that V decreases each loop.
Structural descent for recursion: argument value shrinks in a well-founded order.
Bounded loops – explicit counter reaches 0.

Guarantees reliability in safety-critical systems.
Forms the basis for formal verification tools (Hoare logic, model checkers).
Bridges specification (WHAT) and code (HOW).

Correct algorithms avoid catastrophic failures (e.g., aerospace, medical devices).
Trade-off: exhaustive proofs vs. development time.
Encourages defensive programming and rigorous thinking.