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} iff for all ρ: tr(Pρ) ≤ tr(Q · ⟦S⟧(ρ)) Success amplifies.

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: {P} measure M in q, x := outcome {Σₘ Mₘ P Mₘ†} Measurement outcome captured.

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

Loop: {inv ∧ guard} body {inv} ──────────────────────────── {inv} while guard do body {inv ∧ ¬guard}

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

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

Symbols.

Symbol	Unicode	Name	Meaning
{P} S {Q}	—	Triple	Hoare assertion
ρ	U+03C1	State	Density operator
⊑	U+2291	Löwner	Matrix order
†	U+2020	Dagger	Adjoint

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.