A precise statement of the effects that an individual program is required to achieve. It should clearly state what the program is to do without making any commitment as to how this is to be done. For a program that is intended to terminate, the program specification can take the form of an input-output specification that describes the desired mapping from the set of input values to the set of output values. For cyclic programs, which are not designed to terminate, it is not possible to give a simple input-output specification; normal practice is to focus attention on the individual functions performed by the program during its cyclic operations.

For both terminating and cyclic programs a variety of notations have been employed for program specifications, ranging from natural language with embedded equations and tables to formal notations such as those based upon first-order predicate calculus.