Verification Condition

A logical formula whose validity implies that a program satisfies its specification. Generated mechanically from annotated code in Hoare-style program verification and discharged by theorem provers.

In this vault

Backlinks

Termination Proof line 8
Assigning Meanings to Programs line 29

Linked Pages

Termination Proof

A formal demonstration that a program halts on all inputs of interest, typically via a well-founded measure that strictly decreases across iterations or recursive calls. Complements partial correctness to yield total correctness.

In this vault

Hoare Logic

Axiomatic program-verification system based on Hoare triples {P}C{Q}; direct descendant of Floyd’s edge-assertion method.

In this vault

Assigning Meanings to Programs

Reference: Robert W. Floyd (1967). Proceedings of Symposia in Applied Mathematics, Vol. 19, pp. 19-32 (AMS). Source file: FloydMeaning.pdf. URL

Summary

Floyd’s foundational paper establishes a rigorous, axiomatic basis for proving properties of programs — correctness, termination, equivalence — by attaching propositions (tags) to the edges of a flowchart. A verification condition for each command type guarantees that if the tag on its entrance edge is true when control arrives, then the tag on its exit edge is true when control leaves. Induction over execution then proves global properties like “if initial values satisfy R1, final values satisfy R2”.

The paper defines completeness and consistency of a semantic definition, gives general axioms (axioms 1-4 and corollaries), and derives verification conditions for assignment, conditional branch, join, start, and halt in a simple flowchart language, then extends the approach to fragments of ALGOL. It is a foundational work in axiomatic semantics, directly inspiring Hoare logic.

Key Ideas

Interpretation = mapping from flowchart edges to propositions.
Verification condition per command type enforces local soundness.
Global correctness by induction over execution steps.
Semantic definition should be complete and consistent.
Termination proofs by showing a well-founded quantity strictly decreases.

Connections

Language Workbenches
Agent-Oriented Programming
Verifiable Semantics
Code as Data
Intent Formalization - A Grand Challenge for Reliable Coding — Floyd/Hoare specs as the LLM-era correctness oracle
Making Smart Contracts Smarter — semantic-gap diagnostics in a blockchain setting
Hoare Logic

Conceptual Contribution

Claim: A programming language’s semantics can be defined independently of any implementation by attaching propositions to flowchart edges and constructing per-command verification conditions; global program properties then follow by induction.
Mechanism: Flowchart interpretation as a map from edges to propositions; four general axioms governing verification conditions; derivation of V_c for assignment, branch, join, start, halt; extension to an ALGOL subset (conditional, goto, for, compound, declarations); termination via well-founded decreasing quantities.
Concepts introduced/used: Axiomatic Semantics, Verification Condition, Strongest Verifiable Consequent, Consistency and Completeness, Inductive Assertions, Termination Proof
Stance: foundational / formal-semantic
Relates to: Direct ancestor of Hoare logic and of every verifiable-semantics move in the vault, including Verifiable Semantics for ACLs which transports Floyd/Hoare-style program semantics into the ACL-conformance question. Foundational for Foundations of Logic Programming - Lloyd and reasoning tools in A Modular Approach to Metatheoretic Reasoning for Extensible Languages.