= Formal verification
Establishing specified properties of a system using <formal proofs> about a precise model. <Formal verification> connects an implementation to a <formal specification>; correctness of the model and its assumptions still matters when applying the result to a physical system.
For a small example, the <summation loop verification> below starts with executable steps and asks two separate questions: does any returned value satisfy the <postcondition>, and does execution reach that return? A <loop invariant> answers the first; a <loop variant> answers the second. This turns an unbounded family of permitted <inputs> into a few reusable proof obligations.
The model must specify <programming language semantics>, including the meaning of <variable assignments>, comparisons and <integer arithmetic>. A proof about exact mathematical <integers> need not describe a machine that wraps on <integer overflow>. Similarly, a correct <formal proof> of a weak or mistaken <formal specification> does not establish the intended behavior. Choosing the right <formal specification> and relating the model to the implemented system remain substantive tasks.
<Software testing> examines chosen executions and can expose a <counterexample>. A <formal proof> instead justifies a statement throughout its stated model; it does not require executing every permitted <input>. This makes <formal verification> valuable when rare boundary cases matter, while <software testing> can still reveal an incorrect model or misunderstood requirement.
In 1969, <Tony Hoare> presented rules for <variable assignment>, composition and iteration in a small <programming language>. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.<An Axiomatic Basis for Computer Programming by Tony Hoare>[Hoare, An Axiomatic Basis for Computer Programming, §2 Computer Arithmetic, pp. 576–577; §§3.1–3.4, pp. 577–578; §4 General Reservations, pp. 578–579]{ref}
Back to article page
