Program Verification: Invariants, Semantics, and Local Reasoning

A program is a mathematical object only after its operations have been given a precise interpretation. Verification then relates that interpretation to a specification of the required behavior.

The central questions are concrete. What does the program assume about its input? What must hold when it finishes? Must it finish? Which parts of memory can it change?

The history of deductive verification developed formal tools for answering these questions, then extended them to increasingly substantial software.

Before Hoare logic

Alan Turing's 1949 discussion of checking a large routine already considered reasoning about program behavior. Robert Floyd's 1967 work attached assertions to flowcharts and formulated conditions under which they establish correctness.

C. A. R. Hoare's 1969 axiomatic account organized program reasoning around statements now written

Portrait of C. A. R. Hoare — **C. A. R. Hoare (1934–2026)** Rules connecting commands with preconditions and postconditions.

Sources and credit for C. A. R. Hoare

Nano412, released into the public domain, via Wikimedia Commons Image source · Public domain · Biographical dates

\{P\}\ C\ \{Q\}.

The precondition $P$ describes an initial state, $C$ is a command, and $Q$ is a postcondition.

For partial correctness, the meaning is conditional: if execution starts in a state satisfying $P$ and terminates normally, its final state satisfies $Q$ .

Total correctness additionally requires termination, under the specified semantic treatment of the command. The difference cannot be omitted when interpreting a verified program.

Assignment and substitution

For a simple assignment in a suitable language, the rule

\{Q[E/x]\}\ x:=E\ \{Q\}

works backward from the desired postcondition.

If the command is $x:=x+1$ and the desired result is $x>10$ , substituting the expression into the postcondition gives the precondition $x+1>10$ .

The rule assumes a precise meaning for expressions and assignment. With machine integers, overflow behavior must be included. With expressions that have side effects, the simple presentation may require refinement.

The mathematics establishes a property of the modeled operation, not of every implementation that happens to use the same printed notation.

A loop with a meaningful invariant

Consider a program over unbounded natural-number arithmetic:

text

i := 0
s := 0
while i < n:
    i := i + 1
    s := s + i

Assume $n\ge0$ is fixed during execution. The intended postcondition is

2s=n(n+1).

Use the invariant

0\le i\le n \quad\land\quad 2s=i(i+1).

Initialization establishes it because $i=s=0$ .

For preservation, suppose the old value of $i$ is $k<n$ . After the increment, $i=k+1$ . The new sum is $s'=s+k+1$ , so

2s'=k(k+1)+2(k+1)=(k+1)(k+2).

Thus the equality holds with the new value of $i$ . The bounds are preserved as well.

When the loop exits, the invariant gives $i\le n$ while the false guard gives $i\ge n$ . Hence $i=n$ , and the desired postcondition follows.

This proves partial correctness. To establish termination, use the natural-number measure $n-i$ . It is nonnegative whenever the loop is reached and decreases strictly on each iteration. A strictly descending infinite sequence of natural numbers is impossible.

The proof explains why the invariant has its particular form. It records the mathematical relationship between the completed iterations and the accumulated result.

Dijkstra and weakest preconditions

Edsger Dijkstra's guarded-command work in the 1970s developed a calculus for deriving programs through their specifications.

Portrait of Edsger W. Dijkstra — **Edsger W. Dijkstra (1930–2002)**

Sources and credit for Edsger W. Dijkstra

Hamilton Richards. Via Wikimedia Commons. Image source · CC BY-SA 3.0 · Biographical dates

The weakest precondition $\operatorname{wp}(C,Q)$ describes the states from which command $C$ is guaranteed to terminate with $Q$ , in the usual total-correctness interpretation. Weakest liberal preconditions separate the corresponding partial-correctness account.

For sequential composition,

\operatorname{wp}(C;D,Q) = \operatorname{wp}\bigl(C,\operatorname{wp}(D,Q)\bigr).

This equation explains backward calculation through a sequence. The original guarded-command text also places nondeterminacy and program derivation within the method.

A calculus does not automatically discover useful invariants or termination measures for every loop. Those remain mathematical problems, and unrestricted program verification inherits computability limits.

The method nevertheless makes obligations explicit and allows automation to discharge many local consequences.

Aliasing and the heap

Pointers introduce relationships between names and mutable locations. If two pointer variables refer to the same cell, writing through one changes what is observed through the other.

Hoare-style reasoning can model this behavior. The problem is not that ordinary Hoare logic assumes aliasing never occurs. The problem is how to express and compose useful specifications without repeatedly describing the entire heap.

Rod Burstall's earlier work contributed to reasoning about list structures and storage. Separation logic developed through work by John Reynolds, Peter O'Hearn, Samin Ishtiaq, and others, with important connections to David Pym's bunched implications.

Portrait of John C. Reynolds — **John C. Reynolds (1935–2013)**

Sources and credit for John C. Reynolds

original picture taken by Andrej Bauer , cropped by romanm ( talk ). Via Wikimedia Commons. Image source · CC BY-SA 2.5 · Biographical dates

Portrait of Peter O'Hearn — **Peter O'Hearn (b. 1963)**

Sources and credit for Peter O'Hearn

Duncan.Hull. Via Wikimedia Commons. Image source · CC BY-SA 4.0 · Biographical dates

Its assertions describe how memory can be divided into independently described regions.

Separating conjunction and the frame rule

Write $x\mapsto v$ for an owned heap cell at address $x$ containing $v$ .

The assertion

(x\mapsto v)*(y\mapsto z)

describes two disjoint heap portions. In this simple setting it entails that $x$ and $y$ are distinct addresses.

A local update has the specification

\{x\mapsto v\}\ [x]:=w\ \{x\mapsto w\}.

The frame rule permits the untouched region to be retained:

\{(x\mapsto v)*(y\mapsto z)\}\ [x]:=w\ \{(x\mapsto w)*(y\mapsto z)\}.

The rule requires its usual side conditions, including that the command does not modify variables on which the framed assertion depends, and it relies on a suitable local semantics for the commands.

If $x=y$ , the separating precondition is unavailable. The proof has not ignored aliasing; it has expressed the required disjointness in the assertion itself.

Recursive predicates extend the idea to lists and trees. Concurrent separation logics, including O'Hearn's later work, use related ideas to control interference and ownership across concurrent computations.

CompCert: preserving program behavior

Xavier Leroy's CompCert project, developed with collaborators from the mid-2000s onward, formally verifies major compiler transformations.

Portrait of Xavier Leroy — **Xavier Leroy (b. 1968)**

Sources and credit for Xavier Leroy

David Van Horn. Via Wikimedia Commons. Image source · CC BY 2.0 · Biographical dates

The central kind of theorem relates the semantics of a supported source program to the semantics of the generated target code. The project documentation specifies the compiler's scope and guarantees.

Such a theorem does not show that an arbitrary source program meets its intended application specification. It establishes the appropriate semantic preservation relationship for the verified compilation path, with conditions addressing source behavior and the modeled execution environment.

The distinction is practical. If a source program has been proved to implement an algorithm correctly, compiler correctness helps connect that source-level proof to executable code. Unsupported operations, external components, and machine assumptions still need attention.

Gerwin Klein and the seL4 team reported a major functional-correctness verification in 2009. The work connected a kernel implementation to an abstract specification through refinement proofs.

Later developments extended the assurance story in several directions. The project's proof overview distinguishes functional correctness, security-related properties, supported configurations, and assumptions.

A dated result should be stated for its verified artifact and configuration. It should not be expanded into a claim that every operating system component, hardware device, application, or side channel has been verified.

The achievement demonstrates that formal reasoning can address complex implementation behavior. Its credibility depends partly on making the boundaries of the theorem visible.

Specification remains part of the work

A proof can establish exactly the wrong requirement if the specification is mistaken. It can also establish a useful property that is weaker than the phrase “the program is correct” suggests.

Verification therefore includes selecting a semantics, articulating assumptions, checking correspondence with the intended system, and proving the stated property.

Proof assistants and automated solvers support this work in complementary ways. They can check long derivations and solve local obligations, while the larger task still requires mathematical and engineering judgment.

For reactive systems that continue running, a precondition–postcondition view is often insufficient. We next need a language for properties of entire behaviors.

Sources and further reading

Alan M. Turing, “Checking a Large Routine” (1949).
Robert W. Floyd, “Assigning Meanings to Programs” (1967); C. A. R. Hoare, “An Axiomatic Basis for Computer Programming” (1969).
Edsger W. Dijkstra, “Guarded Commands, Nondeterminacy and Formal Derivation of Programs” (1975).
Samin S. Ishtiaq and Peter W. O'Hearn, “BI as an Assertion Language for Mutable Data Structures” (2001).
John C. Reynolds, “Separation Logic: A Logic for Shared Mutable Data Structures” (2002).
Xavier Leroy, “Formal Verification of a Realistic Compiler” (2009); CompCert documentation.
Gerwin Klein and collaborators, “seL4: Formal Verification of an OS Kernel” (2009); seL4 proof scope.