A software specification describes what a component must do without prescribing every detail of how it does it.

Contracts

A function or module can be understood through a contract:

• preconditions describe what callers must provide;
• postconditions describe what the operation guarantees when it succeeds.

For example, a function may require a nonempty list and guarantee that its result is one of the list's elements and is not smaller than any other element.

Invariants

An invariant is a property that must remain true throughout the relevant lifetime of a value, object or system state. If an order total must always equal the sum of its lines, that rule should guide every operation that can modify the order.

Observable behavior and implementation

A specification should focus on behavior that callers can rely on. Internal data structures, helper functions or algorithm choices are implementation details unless the contract intentionally exposes them.

This separation allows implementations to change without forcing callers or tests to change with them.

Specifications guide tests

Tests are examples derived from a specification. They can check normal cases, boundaries and invalid inputs, but the specification remains the source of what counts as correct behavior.

Clear contracts and invariants therefore make both implementation and testing more precise.