A formal specification is a precise, mathematically grounded description of the intended behaviour or structure of a system, written in a language with well-defined syntax and semantics. It allows properties of the system to be stated unambiguously and reasoned about or verified mechanically. Formal specifications underpin formal methods, model checking, and the construction of provably correct software and ontologies.
Content
- Formal specifications are written in notations such as Z, VDM, TLA+, B, or description logics, enabling automated consistency checking and proof. They separate the statement of intent from implementation, allowing requirements to be validated before code exists. In ontology engineering, the OWL axioms themselves constitute a formal specification of a domain.