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.