= Precondition
The condition required of a starting <program state> for a stated correctness guarantee. In the <summation loop verification>, $n\in\mathbb Z$ and $n\geq0$ admit $n=0$ and $n=4$, but exclude $n=-1$. The accompanying model assumes exact <integer arithmetic> and terminating elementary operations. The initial values of $i,s$ need no restriction because initialization overwrites them before use.
A <precondition> is a logical assumption, not automatically an executable check. Writing `require` in a procedure states its contract; an implementation that checks or rejects invalid <inputs> needs that behavior specified too. Weakening a <precondition> admits more starts and therefore demands more proof: dropping $n\geq0$ here makes $n=-2$ a terminating <counterexample> to $2s=n(n+1)$, since initialization returns zero while $n(n+1)=2$.
Back to article page
