Quantum Hoare Logic

Origin. Ying (2011). Program logic for quantum. Partial correctness. Density matrices as states. Foundation for quantum program verification.

Models. Quantum programs with classical control. Preconditions/postconditions as subspaces. Löwner order. Partial density operators.

Formalism.

Quantum state: ρ: density operator (positive, trace ≤ 1). Pure: |ψ⟩⟨ψ|. Mixed: Σᵢ pᵢ |ψᵢ⟩⟨ψᵢ|.

Hoare triple: {P} S {Q} P, Q: projection operators (predicates). Partial correctness.

Validity: {P} S {Q} for partial correctness iff for every ρ: tr(Pρ) ≤ tr(Q · ⟦S⟧(ρ)) + [tr(ρ) − tr(⟦S⟧(ρ))] The bracketed term is the probability that S fails to terminate, and it is precisely what makes this partial: divergence is forgiven, as classically. Total correctness is the same inequality with that term deleted — tr(Pρ) ≤ tr(Q · ⟦S⟧(ρ)) — which additionally demands that ⟦S⟧ be trace-preserving.

Skip: {P} skip {P}

Unitary: {U†PU} q := U[q] {P} Backwards through unitary.

Initialization: {I} q := |0⟩ {|0⟩⟨0|_q} Initialize to |0⟩.

Measurement (case statement): {Pₘ} Sₘ {Q} for every outcome m ───────────────────────────────────────────── {Σₘ Mₘ† Pₘ Mₘ} case (□m · M[q̄] = m → Sₘ) end {Q}

Each dagger goes on the left: Mₘ† Pₘ Mₘ pulls the branch precondition back through the measurement, the same direction as U†PU in the unitary axiom. The forward conjugation Mₘ Pₘ Mₘ† is how states evolve, not how predicates do, and the rule is unsound with the daggers that way round.

Sequence: {P} S₁ {Q} {Q} S₂ {R} ──────────────────────────── {P} S₁; S₂ {R}

Loop: The guard is a two-outcome measurement M = {M₀, M₁}, the loop continuing on outcome 1:

{Q} S {M₀† P M₀ + M₁† Q M₁} ─────────────────────────────────────────────── {M₀† P M₀ + M₁† Q M₁} while M[q̄] = 1 do S od {P}

There is no "inv ∧ ¬guard" to write: projections have no Boolean conjunction unless they commute, and the guard is a measurement rather than a proposition. Invariant Q and exit assertion P are instead combined by the measurement itself, in the single operator M₀† P M₀ + M₁† Q M₁ that serves as both the premise's postcondition and the conclusion's precondition.

Consequence: P' ⊑ P {P} S {Q} Q ⊑ Q' ────────────────────────────────── {P'} S {Q'}

⊑: Löwner order (P ⊑ Q iff Q - P positive).

Symbols.

Metatheory. Sound. Relative completeness. Extensions for total correctness. Probabilistic reasoning.

Applies to. Quantum program verification. Algorithm correctness. Error analysis. Certified quantum software.

Limitations. Infinite-dimensional harder. Approximation. Classical-quantum interface. Tool support developing.

© 2026 Lingenic LLC