Formal specification

A mathematically precise description of a system’s required behavior, written in a formal language so its properties can be analyzed or verified.

Formal language: A language defined by explicit rules for forming and interpreting expressions. A specification uses a formal language to remove ambiguity from requirements.
Temporal logic: A family of logics for expressing how propositions hold across time or sequences of states. Temporal formulas express requirements such as eventual response and perpetual safety.
Formal verification: The use of mathematical methods to prove or check that a system satisfies stated properties. Verification checks whether an implementation or model meets its specification.
Natural language: A language that develops and changes through ordinary human use rather than explicit formal rules. Natural-language requirements are accessible but can leave behavior open to interpretation.
Mathematical logic: The study of formal systems of reasoning, including proof, truth, and inference. Logical rules give specifications precise meanings and support proofs about them.
Hoare logic: A formal system for reasoning about programs using preconditions, commands, and postconditions. Hoare triples specify what a program must establish when its assumptions hold.
Model checking: An automated method that explores a finite-state model to find violations of specified properties. Model checkers can test whether a system model satisfies temporal requirements.
Software testing: The execution of software under selected conditions to find defects or assess behavior. Testing samples executions; a formal specification can state properties for all modeled behaviors.
State machine: A model of a system as states and transitions between those states. State-machine models express how permitted behavior changes over time.
Z notation: A formal specification language based on set theory and first-order predicate logic. Z schemas describe state and operations through mathematical constraints.

Linked from 3 pages

Program verificationRelated: Verification can establish only properties that have been stated precisely enough to check.