= Formal specification
A mathematically precise description of permitted behaviour. A <formal specification> for the <microkernel file-read example>'s service could relate an authorized request to the exact returned <bytes>; a <formal specification> of its <microkernel>'s <IPC> need only describe the protected transport operation. They state different obligations.
For the <summation loop verification>, require a nonnegative <integer> <input> $n$ and a returned value $s$ satisfying $2s=n(n+1)$. The <formal specification> describes what answer is acceptable without requiring this particular loop: another implementation may satisfy the same contract. State separately whether <partial correctness> or <total correctness> is required. A <Hoare triple> packages the <precondition>, the program and the <postcondition>; <Hoare logic> supplies rules for establishing such claims.
Precision alone does not ensure a useful requirement. The <postcondition> $s\geq0$ permits returning zero for every nonnegative <integer> <input>; it does not specify the intended <triangular number>. Conversely, an impossible <precondition> permits no starts, making a universal correctness claim vacuous. Check both that intended <inputs> are admitted and that admitted <outputs> express the intended task.
Back to article page
