A specification is a quadruple: F = < D, R, I, O > where:
| D | = | Input type (domain) |
| R | = | Output type (range) |
| I | = | Input condition |
| O | = | Output condition |
In a program-like form, a specification can be written:
function F(x:D) : set(R)
where I(x)
returns { z | O(x, z) }
= Body
Body is code that can be executed to compute F. A spec is consistent if: &forall (x:D) ( I(x) &rArr F(x) = { z | O(x, z) } )