Formal Specification

Overview

Formal specification uses mathematically precise languages to describe what a system should do, eliminating the ambiguity inherent in natural language requirements. A formal specification serves as a contract between stakeholders and developers, and as a foundation for verification.

Formal vs Informal Specification

| Aspect | Informal | Formal | |--------|----------|--------| | Language | Natural language, diagrams | Mathematical notation | | Ambiguity | Prone to misinterpretation | Unambiguous by construction | | Analysis | Manual review only | Machine-checkable properties | | Audience | All stakeholders | Trained engineers | | Completeness | Hard to assess | Formally verifiable |

Formal specifications are not replacements for informal ones -- they complement each other. Informal descriptions provide intuition; formal ones provide precision.

Specification Languages

Z Notation

Z uses typed set theory and first-order predicate logic. Specifications are organized into schemas that group declarations and predicates.

┌─ Account ─────────────────────┐
│ balance : ℤ                   │
│ owner : PERSON                │
├───────────────────────────────┤
│ balance ≥ 0                   │
└───────────────────────────────┘

┌─ Withdraw ────────────────────┐
│ ΔAccount                      │
│ amount? : ℤ                   │
├───────────────────────────────┤
│ amount? > 0                   │
│ amount? ≤ balance             │
│ balance' = balance - amount?  │
└───────────────────────────────┘

Δ indicates state change; Ξ indicates no change
? suffix denotes input; ! suffix denotes output
Primed variables (balance') represent after-state

VDM (Vienna Development Method)

VDM-SL provides explicit and implicit function/operation definitions with pre/post conditions.

types
  Account :: balance : nat
             owner : Person

operations
  Withdraw(amount : nat) ext wr balance : nat
    pre amount > 0 and amount <= balance
    post balance = balance~ - amount

balance~ refers to the pre-state value
VDM supports proof obligation generation
VDM++ extends VDM-SL with object-oriented features

TLA+ (Temporal Logic of Actions)

TLA+ specifies systems as state machines using temporal logic. Created by Leslie Lamport.

VARIABLE balance

Init == balance = 100

Withdraw(amount) == /\ amount > 0
                    /\ amount <= balance
                    /\ balance' = balance - amount

Next == \E a \in 1..balance : Withdraw(a)

Spec == Init /\ [][Next]_balance

Actions describe state transitions as relations between old and new states
[][Next]_balance means each step is either a Next step or a stuttering step
Particularly strong for distributed and concurrent systems

Alloy

Alloy uses first-order relational logic with transitive closure. Its bounded analysis (via the Alloy Analyzer / SAT solving) finds counterexamples automatically.

sig Account {
  balance: one Int,
  owner: one Person
} {
  balance >= 0
}

pred withdraw[a, a': Account, amount: Int] {
  amount > 0
  amount <= a.balance
  a'.balance = a.balance.minus[amount]
  a'.owner = a.owner
}

check NoOverdraft {
  all a, a': Account, amt: Int |
    withdraw[a, a', amt] implies a'.balance >= 0
} for 5

for 5 bounds the search to 5 atoms per signature
"Small scope hypothesis": most bugs have small counterexamples

Core Concepts

Preconditions and Postconditions

Precondition: what must hold before an operation executes
Postcondition: what must hold after an operation completes
Together they form the operation's contract

A precondition that is true (always satisfied) means the operation is total. A strong precondition restricts when the operation may be invoked.

Invariants

State invariants are predicates that must hold in every reachable state. They constrain the state space and encode domain rules (e.g., "balance is never negative").

Data type invariants: constraints on representation
System invariants: global properties across components
History invariants: constraints on sequences of states

Every operation must preserve invariants: if the invariant holds before, it must hold after.

Refinement maps an abstract specification to a more concrete one while preserving all observable behaviors.

Abstract Spec  ──refinement──>  Concrete Spec  ──refinement──>  Implementation

Data refinement: replace abstract data types with concrete representations. A retrieve function maps concrete states back to abstract states.

Proof obligations for refinement:

Every concrete initial state maps to a valid abstract initial state
Every concrete operation, when translated back, satisfies the abstract postcondition
Concrete invariants are maintained

Operation refinement: strengthen preconditions (accept more inputs) or weaken postconditions (produce more specific outputs) -- actually it is: weaken preconditions (accept more) and strengthen postconditions (promise more).

Completeness

A specification is complete if it defines the system's behavior for all relevant inputs and states. Completeness checking asks:

Are all operations defined for their intended input domains?
Are all state components constrained by invariants?
Does the specification cover all required functionality?

Tools can check for missing cases, undefined expressions, and unreachable states.

Consistency

A specification is consistent if it is free of contradictions:

No invariant contradicts another
Pre/post conditions are satisfiable simultaneously
Initial states satisfy the invariant

Inconsistency means no implementation can satisfy the spec. Z and VDM tools generate proof obligations that, when discharged, guarantee consistency.

Comparison of Languages

| Feature | Z | VDM | TLA+ | Alloy | |---------|---|-----|------|-------| | Foundation | Set theory | Set theory | Temporal logic | Relational logic | | State model | Schemas | Modules | State machines | Signatures | | Concurrency | Limited | Limited | First-class | Limited | | Tool support | CZT, Z/EVES | Overture | TLC, TLAPS | Alloy Analyzer | | Analysis | Proof | Proof + test | Model checking | SAT-based | | Industry use | Security, safety | Embedded | Distributed systems | Design exploration |

Practical Considerations

When to use formal specification:

Safety-critical systems (avionics, medical, nuclear)
Security protocols and cryptographic designs
Complex concurrent/distributed algorithms
Hardware design verification

Incremental adoption: specify the most critical components first. Even partial formalization catches ambiguities and inconsistencies that informal review misses.

Cost-benefit: the upfront cost of formal specification is offset by reduced defects downstream. Studies (e.g., the Tokeneer project with Z) show significant defect reduction with modest specification effort.

Key Takeaways

Formal specifications eliminate ambiguity through mathematical precision
Pre/post conditions and invariants are the building blocks of specifications
Refinement provides a rigorous path from abstract specs to implementations
Different languages suit different problem domains: TLA+ for concurrency, Alloy for structural exploration, Z/VDM for sequential data-oriented systems
Consistency and completeness are checkable properties of specifications