Skip to content

Proof of correctness

A mathematical demonstration that an algorithm satisfies a formal specification, separating partial correctness from the additional obligation to prove termination for total correctness.

Version
v1 · 2026-09-28 · History
Domain-specific #
11527
Domain group
Applied Sciences & Engineering
Origin domain
Computer Science & Software Engineering
Subdomains
Formal Verification, Program Correctness → Computer Science & Software Engineering

Core Idea

A proof of correctness is a mathematical argument that an algorithm meets a formal specification. Correctness is relational: the same algorithm can be correct for one precondition and postcondition and incorrect for another, so the specification is part of the claim.

Partial correctness proves that if execution terminates, the returned result satisfies the postcondition. Total correctness adds termination for every admissible input. A common structure combines loop invariants or inductive hypotheses with a well-founded variant that decreases until the algorithm stops.

The proof concerns an abstract algorithm and formal semantics. It does not automatically establish that one machine implementation is free of compiler faults, memory exhaustion, hardware errors, or an inaccurate specification. Testing remains valuable but samples executions rather than quantifying over all of them.

Structural Signature

Sig role-phrases:

  • formal specification. Defines preconditions, postconditions, invariants, and required behavior. Constitutive standard. If altered: A proof without a specification can establish an irrelevant property.
  • algorithm semantics. Fixes the mathematical meaning of program steps and states. Constitutive carrier. If altered: Reasoning about source syntax without semantics cannot connect execution to claims.
  • inductive invariant. Relates reachable states to the specification throughout iteration or recursion. Characteristic proof bridge. If altered: An invariant too weak cannot imply the postcondition.
  • partial-correctness argument. Shows that every terminating execution from a valid input satisfies the result condition. Constitutive obligation. If altered: It remains compatible with nontermination.
  • termination argument. Uses a well-founded measure or equivalent reasoning to show all relevant executions end. Required for total correctness. If altered: Omitting it cannot support a total-correctness claim.

What It Is Not

  • Not testing. Observed cases cannot generally quantify over every admissible input and path.
  • Not termination alone. An algorithm can halt reliably with the wrong result.
  • Not partial correctness alone. A total claim also needs a termination argument.
  • Not specification validation. A proven program can faithfully implement a mistaken requirement.

Scope of Application

The method applies to formally specified algorithms and programs whose semantics support deductive, automated, or mechanically checked reasoning.

  • Algorithm design. Proves input–output properties and termination.
  • Hoare logic. Uses assertions and triples over imperative programs.
  • Proof assistants. Mechanically check formal arguments.
  • Compiler verification. Relates source and target semantics.
  • Safety-critical software. Establishes selected properties beyond testing.

Clarity

Correctness proof separates four questions: what is required, what the algorithm means, whether results satisfy the requirement, and whether computation ends. It also exposes the assurance boundary between algorithm, implementation, platform, and specification.

Manages Complexity

A program has many paths and states. Invariants and compositional proof rules summarize whole families of executions, replacing exhaustive enumeration with a finite chain of obligations whose assumptions and conclusions can be checked.

Abstract Reasoning

  1. Formalize admissible inputs, required outputs, and operational or denotational semantics.
  2. Decompose the algorithm into proof obligations using invariants and contracts.
  3. Prove initialization, preservation, and postcondition consequences for every path.
  4. For total correctness, provide a well-founded decreasing measure or equivalent termination proof.
  5. Audit the trusted base and confirm that the specification expresses the intended requirement.

Knowledge Transfer

Proof methods transfer literally across algorithms when semantics and specifications are restated. A proof about an abstract routine does not automatically transfer to a compiled binary or resource-bounded environment; refinement links must be proved separately.

Examples

Canonical

For a sorting loop, the invariant states that the processed prefix is sorted and contains exactly the processed input elements. Initialization and preservation are proved; at termination the prefix is the whole array, yielding sortedness and permutation.

Mapped back: formal specification → sorted permutation; algorithm semantics → array-loop updates; inductive invariant → sorted processed prefix; partial-correctness argument → postcondition at loop exit; termination argument → unprocessed length decreases.

Applied / In Practice

A search enumerates positive integers and returns only after finding an odd perfect number. Its return value can be proved valid, but termination cannot be proved without establishing that such a number exists; it is partially, not totally, correct.

Mapped back: formal specification → return an odd perfect number; algorithm semantics → sequential enumeration; inductive invariant → all earlier candidates checked; partial-correctness argument → verified returned witness; termination argument → not established.

Structural Tensions

T1: mathematical completeness vs. trusted implementation stack. An algorithm proof may leave compilers, hardware, and resources outside its model. Diagnostic: What exact artifact and semantics does the theorem cover?

T2: strong specification vs. proof cost. Richer properties improve assurance while multiplying formalization and proof obligations. Diagnostic: Which properties are decision-critical?

T3: partial result vs. termination. A returned result can be correct even when some executions never return. Diagnostic: Is liveness part of the claimed contract?

Structural–Framed Character

Proof of correctness is structural-leaning. Deduction and semantics are formal, while the chosen specification and assurance boundary reflect human goals. It has high evaluative weight in safety contexts and strong institutional tooling. Its character: universal behavioral assurance relative to an explicit formal contract.

Structural Core vs. Domain Accent

Skeletal core. Derive that every admissible transformation path preserves an invariant and reaches a required condition, with progress proved separately.

Domain-bound accent. Algorithms, states, Hoare triples, loop invariants, termination variants, and formal semantics define the method.

Why not prime. Verification travels, but proof of program correctness is a specific formal-computing practice.

This entry is a kind of Argument.

  • Invariant. A preserved property bridges local program steps to a global postcondition.
  • Well-founded descent. Termination follows from progress in an order with no infinite descent.
  • No canonical parent edge is asserted in the current DAG.

Relationships to Other Abstractions

Local relationship map for Proof of correctnessParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Proof of correctnessDOMAINPrime abstraction: Argument — is a kind ofArgumentPRIME

Current abstraction Proof of correctness Domain-specific

Parents (1) — more general patterns this builds on

  • Proof of correctness is a kind of Argument Prime

    Proof of correctness is a domain-specific kind of argument under the frozen identity and differentia.

Hierarchy path (1) — routes to 1 parentless root

Neighborhood in Abstraction Space

Proof of correctness sits in a moderately populated region (40th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Formal Models & Logical Foundations (33 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • Software testing. Tell: Are all admissible executions covered deductively or only sampled empirically?
  • Formal verification. Tell: Is the broad field meant or one correctness proof artifact?
  • Model checking. Tell: Is a finite state model exhaustively explored or a deductive proof constructed?
  • Type safety. Tell: Does the theorem prevent one class of errors or establish the full functional specification?

References

  • Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Correctness_(computer_science) (revision 1355883744).
  • Preserved source candidate: https://dl.acm.org/ft_gateway.cfm?id=356881
  • Preserved source candidate: http://www.ece.cmu.edu/~koopman/des_s99/sw_testing/
  • Preserved source candidate: https://books.google.com/books?id=l5FZxDY3yi0C&q=correctness
  • Preserved source candidate: https://books.google.com/books?id=6YAXDQAAQBAJ&q=correctness
  • Preserved source candidate: https://www.coopertoons.com/education/haltingproblem/haltingproblem.html
  • Preserved source candidate: https://stanford.library.sydney.edu.au/entries/computer-science/

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.