Quantum Hoare Logic

Quantum Hoare logic generalizes the triple $\{P\}\,C\,\{Q\}$ to programs manipulating quantum states. Predicates are effects: Hermitian operators satisfying $0\preceq P\preceq I$. For a normalized state $\rho$, the quantity $\mathrm{tr}(P\rho)$ is the probability of the effect's measurement outcome. It also serves as a quantitative satisfaction value.

Let $\mathcal E=\llbracket C\rrbracket$ be a completely positive, trace-nonincreasing map collecting terminating executions, as in denotational semantics. The meaning of a triple depends on whether nontermination is permitted.

Partial and total correctness

Partial correctness holds when, for every subnormalized input $\rho$,

The final two terms give credit for probability mass lost through nontermination. Omitting this compensation changes the definition to total correctness:

For trace-preserving programs the two conditions coincide. A total-correctness triple does not impose termination on every input independently of its precondition: $P=0$ gives a trivial triple. With $P=I$, the total inequality forces termination with probability one and satisfaction of $Q$ with probability one on every normalized input.

A map describing postselection also loses trace, but interpreting that loss as nontermination requires an explicit program model. Normalizing a successful branch and silently applying these formulas would change their meaning.

Examples and predicate transformers

For the Pauli $X$ gate, take $P=\lvert0\rangle\langle0\rvert$ and $Q=\lvert1\rangle\langle1\rvert$. Since $X^\dagger QX=P$, both triples hold with equality for every input.

For a program that never terminates, $\mathcal E(\rho)=0$. Every partial-correctness triple holds because $P\preceq I$. Total correctness can hold for all inputs only when $P=0$. This example exposes why the compensation term matters.

Writing $\mathcal E^*$ for the trace adjoint, the equivalent operator conditions are

for partial correctness, and $P\preceq\mathrm{wp}_C(Q)=\mathcal E^*(Q)$ for total correctness. See weakest preconditions for backward calculation rules.

Limitations

Measurement branches must be combined using their quantum operations, with classical outcomes retained when the specification observes them. Loops require invariants and, for appropriate total specifications, termination arguments. These introductory examples illustrate semantic validity; they are not machine-checked proofs of a compiler or hardware implementation. A proof system's soundness and completeness require separate theorems.

References

• Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems 33(6), 1-49 (2011). DOI: 10.1145/2049706.2049708.
• Ellie D'Hondt and Prakash Panangaden. Quantum Weakest Preconditions. Mathematical Structures in Computer Science (2006). arXiv:quant-ph/0501157.