The purpose of a program is to achieve a desired state transformation. A specification is a ``declarative'' description of such a transformation, that is it specifies the desired net effect of a transformation without concerning itself about how this effect is achieved using the available commands.
The classical method of C.A.R.Hoare ([5],[1])presents a specification as a pair (P,Q) of expressions in the predicate logic over the underlying data structure. The idea is that a command C satisfies the specification (P,Q), if for any state satisfying P the state achieved after executing C satisfies Q. However, the possibility that must be taken into account, so we distinguish between partial correctness
and total correctness:
Thus given a specification (P,Q), it may be considered the programmers job to solve it by finding a program X such that , or even is true.