= Postcondition
The condition required of a final <program state> when a program finishes under its <precondition>. The <summation loop verification> requires returned value $s$ to satisfy $2s=n(n+1)$ and preserves the <input> $n$. Relating the answer to the original <input> matters: allowing the program to replace $n$ by zero would change the intended contract.
A <postcondition> alone gives no promise of <algorithm termination>. It also need not specify a unique <output>: $s\geq0$ allows many answers, while the exact <triangular number> equation determines one <integer> answer for each permitted $n$. Stronger <postconditions> express more obligations; proving only a weaker consequence cannot justify the stronger requirement.
Back to article page
