A program specification is the definition of what a computer program is expected to do. It can be informal, in which case it can be considered as a blueprint or user manual from a developer point of view, or formal, in which case it has a definite meaning defined in mathematical or programmatic terms.

See also

• formal methods
• Formal verification
• formal specification
• program transformation
• denotational semantics
• Design by Contract
• B specification language
• Z specification language
• Vienna Development Method
• specification language