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 (nothingbad ever happens) and liveness properties (something good eventually happens). The distinction between safety and liveness is not merely technical — it is a fundamental classification of what systems can promise. Safety properties can be violated in finite time; liveness properties require infinite time to confirm. No specification language that cannot express both can claim to describe systems as they actually behave.

The Design Space of Specification Languages

The landscape of specification languages is richer than the mainstream software engineering curriculum suggests. Alloy, developed by Daniel Jackson at MIT, uses relational logic to describe structural constraints on complex data structures. It is not a language for proving theorems about dynamic behavior; it is a language for finding counterexamples to structural claims. In a world where most system failures are caused by unexpected interactions between components, Alloy's counterexample-finding orientation is often more useful than theorem-proving.

Promela, the specification language of the Spin model checker, is designed for protocol verification. It describes concurrent processes communicating through channels, and Spin exhaustively checks that the specified protocol satisfies its claimed properties. The language is small by design — its simplicity is what makes exhaustive model checking tractable.

At the extreme of expressive power, Coq and Agda are not merely programming languages; they are specification languages in which programs are proofs. The Curry-Howard correspondence makes these languages into environments where the specification and the implementation are the same object, separated only by the level of abstraction at which you read them. This is the ultimate compression of the specification/implementation gap.

Specification Languages as Systems Theory

Specification languages are not merely tools for software engineers. They are the formal embodiment of a question that systems theory asks in every domain: how do you describe what a system should do, separately from what it actually does, in a way that permits comparison between the two?

In Control Theory, this question is answered by transfer functions and stability criteria. In Economics, by equilibrium models and welfare theorems. In Biology, by fitness landscapes and regulatory network models. Each of these is a specification language for a different class of system. The formal languages of computer science — Z, TLA+, Alloy, Coq — are simply the most explicit and mechanically checkable instances of a universal practice: describing intended behavior in a formalism that can be compared against observed behavior.

The divergence between specification and implementation is not a software problem. It is a systems problem. Any system whose behavior is complex enough to be non-obvious — a cell, a market, a climate model, a society — requires some external representation against which its behavior can be evaluated. Specification languages make this representation explicit and checkable. In doing so, they do for designed systems what scientific models do for natural systems: they provide a formal target that the system can miss.

The failure of most software projects is not a failure of coding. It is a failure of specification — the inability to state clearly what the system should do before building it. The resistance to formal specification in industry is not a rejection of rigor; it is a rejection of the uncomfortable fact that most systems, when their requirements are made explicit, are revealed to be incoherent. Specification languages do not merely verify systems. They force the recognition that many systems, as specified, are not worth building.