Quantum Programming Logic

Origin. D'Hondt and Panangaden (2006), Ying (2012). Hoare-style logic for quantum programs. Quantum weakest precondition. Verification of quantum algorithms. Foundation for quantum program correctness.

Models. Program logic for quantum. Classical Hoare: {P} C {Q} for classical programs. Quantum Hoare: {ρ} C {σ} for quantum programs. Density matrices as assertions. Quantum operations as commands.

Formalism.

Quantum state assertions: ρ: density matrix (positive, trace 1). ρ ⊑ σ: Löwner order (σ - ρ positive semidefinite). Partial correctness: {ρ} C {σ} means if input satisfies ρ, output satisfies σ.

Quantum commands:

q := |0⟩ (initialization)
q := U[q] (unitary transformation)
measure q (measurement)
if □m=i → Pᵢ fi (measurement-based conditional)

Quantum Hoare rules: Initialization: {I} q := |0⟩ {|0⟩⟨0|}

Unitary: {U†ρU} q := U[q] {ρ}

Measurement: {Σᵢ MᵢρMᵢ†} measure q {ρ}

Sequential: {ρ} C₁ {σ} {σ} C₂ {τ} ───────────────────────── {ρ} C₁; C₂ {τ}

Quantum weakest precondition: wp(C, ρ) = weakest state such that {wp(C,ρ)} C {ρ}

Total correctness: Loops: require termination proof. Quantum while: fixed-point semantics.

Symbols.

Symbol	Unicode	Name	Meaning
ρ, σ	U+03C1, U+03C3	Density matrix	Quantum state
U	—	Unitary	Quantum gate
M	—	Measurement	Observable
⊑	U+2291	Löwner order	State comparison
†	U+2020	Dagger	Adjoint
\|0⟩	—	Zero state	Initial qubit
wp	—	Weakest precondition	Precondition

Metatheory. Soundness: valid triples preserve quantum semantics. Completeness: for finite-dimensional. Quantum wp well-defined. No cloning: classical rules don't apply directly. Entanglement complicates local reasoning.

Applies to. Quantum algorithm verification. Quantum error correction. Quantum cryptography. Quantum compilers. Formal methods for quantum.

Limitations. Infinite-dimensional harder. Continuous parameters. Error/noise modeling separate. Tool support emerging. Scalability challenges. Entanglement across qubits.