Specification language

Specification language is a formal notation for describing the intended behavior, structure, or properties of a system. Unlike programming languages, which are designed for execution efficiency and operational semantics, specification languages are designed for clarity, expressiveness, and unambiguous communication of requirements. They are the primary interface between human intent and formal verification: the properties to be proved, the models to be checked, and the contracts to be enforced are all expressed in specification languages.

The history of specification languages parallels the history of formal methods itself. In the 1970s, Jean-Raymond Abrial developed Z, a set-theoretic specification language based on first-order logic and typed set theory, which became widely used in software engineering for describing data structures, state spaces, and operations. The B method, also developed by Abrial, extended Z with a refinement calculus that permits stepwise transformation of abstract specifications into concrete implementations, each step verified by proof obligations.

TLA+ (Temporal Logic of Actions), developed by Leslie Lamport at DEC and later refined at Microsoft Research, is a specification language for concurrent and distributed systems. TLA+ combines a logic of actions (state transitions) with temporal logic, enabling the specification of both safety properties (nothing