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 effects. Löwner order. Partial density operators.

Formalism.

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

Hoare triple: {P} S {Q} P, Q: quantum predicates — effects, Hermitian operators with 0 ≤ P ≤ I. 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. Ying (2011) proved the system sound and complete for quantum while-programs: every valid partial-correctness triple is derivable, with completeness established through the weakest-precondition operator, which for a program S is the adjoint superoperator ⟦S⟧† characterized by tr(⟦S⟧†(P)ρ) = tr(P⟦S⟧(ρ)) for all ρ — the Heisenberg picture dual to the Schrödinger-picture denotation. The construction rests on Selinger's (2004) observation that partial density operators under the Löwner order form a CPO with least element 0 on which superoperators are Scott-continuous, so the while-loop denotation exists as a least fixed point and the loop rule is sound. Total correctness is the same inequality without the divergence term, and its completeness requires an additional ranking argument for loops. D'Hondt and Panangaden (2006) had already established that quantum predicates should be the effects, positive operators below I, and that the predicate transformer is the adjoint. Zhou, Yu, and Ying (2019) gave a sound and relatively complete variant restricted to projections, where satisfaction is exact rather than graded.

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

Limitations. The assertion language has no conjunction: by Kadison's antilattice theorem the self-adjoint operators are lattice-ordered only in the commutative case, so P ⊓ Q generally does not exist and there is no rule for combining two established postconditions, which is why the loop rule must fuse invariant and exit condition into M₀†PM₀ + M₁†QM₁ rather than writing "invariant and not guard". Satisfaction is graded — tr(Pρ) is a probability, not a truth value — so a triple asserts an inequality between probabilities; a state satisfies P outright only when P is a projection containing the support of ρ. There is no frame rule: entangled registers cannot be reasoned about separately, and separation-logic variants require separability side conditions. Completeness assumes the assertion language contains arbitrary effects, 2^n × 2^n operators with no finite syntactic presentation, so proof obligations are exponential in register size and need not lie in any decidable theory.

© 2026 Lingenic LLC