Formal Specification

Rigorously define what a system "should do" using mathematical notation

What is Formal Specification

Formal specification is a methodology that rigorously defines the behavior of software and systems using mathematical foundations such as predicate logic, set theory, and algebra. While natural language specifications can be interpreted differently by different readers, formal specifications are mathematically unambiguous, ensuring all stakeholders share an identical understanding.

The purpose of formal specification is to define 'what the system should do (What)' without including 'how to implement it (How).' This separation allows focusing on the essence of design, enabling specification development that is not constrained by implementation methods.

Core Concepts

Type Definition and Invariants: Define the structure of data as types and describe constraints (invariants) that the type must always satisfy. For example, constraints such as "age is an integer between 0 and 150" or "email addresses are unique" are expressed mathematically. This ensures that invalid data states cannot exist in the first place.

Preconditions and postconditions: Explicitly state conditions that must hold before an operation (function) is executed (preconditions) and conditions guaranteed after execution (postconditions). This clarifies the responsibility scope of each operation and rigorously defines boundaries between modules.

Stepwise Refinement: A process of stepwise refinement from abstract specifications to concrete designs. At each step, the consistency with the upper-level specification can be mathematically verified, ensuring that the intent of the specification is accurately preserved through implementation.

Major Specification Languages

VDM-SL (Vienna Development Method)

One of the oldest formal specification languages, developed at IBM's Vienna Laboratory in the 1970s. It features rich data types such as sets, maps, and sequences, along with operation definitions using preconditions and postconditions. It is standardized as ISO/IEC 13817-1.

-- User registration specification example
RegisterUser(email: Email, name: seq1 of char) uid: UserId
  pre email not in set dom userDB
  post userDB = userDB~ munion {uid |-> mk_User(email, name)}
       and uid not in set dom userDB~

In this example, the preconditions (the email address must not already be registered) and postconditions (a new user is added to the user DB) of the RegisterUser operation are rigorously defined.

TLA+

A specification language conceived by Leslie Lamport (2013 Turing Award recipient). Based on Temporal Logic of Actions, with particular strength in specifying concurrent and distributed systems. Gained significant attention in the industry after adoption by Amazon Web Services for large-scale distributed system verification.

B-Method

A specification and stepwise refinement technique based on set theory and predicate logic. The key feature is that each stepwise refinement can be mathematically verified. Has a track record in the Paris Metro Line 14 unmanned operation system and railway signaling systems worldwide.

Z Notation / Alloy

Z notation is a specification method developed at the University of Oxford, based on set theory and predicate logic. It describes states and operations using structures called schemas. Alloy is a lightweight formal method developed by Daniel Jackson at MIT, based on relational logic, enabling automated analysis through model exploration.

Problems Solved by Formal Specification

Elimination of specification ambiguity: In natural language specifications, phrases like 'users can retry any number of times' can be interpreted in multiple ways, but in formal specifications, constraints are uniquely determined. Discrepancies in understanding between clients, designers, and implementers are eliminated.

Detecting contradictions at the design stage: Formal specifications can be mechanically verified. Conflicting conditions and unreachable states can be detected before writing a single line of code. Many bugs discovered after implementation actually originate from contradictions at the specification stage.

Systematic derivation of test cases: When preconditions and postconditions are rigorously defined, test cases including boundary values and edge cases can be systematically derived. The risk of test coverage gaps is reduced.

Traceability of change impact: When specifications are formally written, the impact of changes to one specification on other parts can be mechanically analyzed. The scope of change propagation becomes predictable, reducing the risk of regression bugs.

Barriers to Adoption

Despite the effectiveness of formal specification, its adoption in general software development has been limited. The main barriers include the cost of learning mathematical notation, the increase in initial effort for specification writing, and the difficulty of integrating into existing development workflows.

As a result, formal specification has been primarily applied in safety-critical domains (aviation, railway, medical devices, nuclear power). However, recent developments in LLMs (Large Language Models) are changing these barriers.

IID Systems Research

IID Systems is researching an approach that uses VDM-SL formal specifications as contracts between AI agents. By having AI assist with writing and verifying formal specifications, we are exploring the potential to lower the barrier of mathematical expertise and bring the benefits of formal specification to a wider development audience.