Floyd–Hoare Logic for Quantum Programs

Paper information (2011, TOPLAS 33(6), Article 19, pp. 1–49) — Mingsheng Ying. DOI; arXiv:0906.4586

Work

The paper generalizes the classical Floyd–Hoare triple to quantum programs. Quantum assertions are operators describing measurement properties, and program statements transform assertions through inference rules. The system treats both partial and total correctness. It also uses quantum weakest preconditions to establish relative completeness: given the semantics and an expressive enough assertion language, semantically valid properties can be derived by the rules.

Contributions

• Quantum Floyd–Hoare triples and inference rules for quantum programs.
• Coverage of both partial correctness and total correctness.
• Assertion reasoning for quantum operations, measurement, and loops.
• A relative-completeness result based on quantum weakest preconditions.

Limits

Relative completeness assumes that the assertion language can express the required weakest preconditions; it does not mean that proofs can be generated automatically. Loops still need suitable invariants and termination arguments, and the quantum model, classical variables, nontermination, and noise assumptions must be stated. A formal proof does not by itself establish the correctness of a particular compiler or hardware implementation.

Connections

The paper develops the predicate-transformer perspective of Quantum Weakest Preconditions into a compositional program logic. It shares an imperative-program focus with Reasoning About Imperative Quantum Programs, but gives a more systematic Floyd–Hoare rule system and relative-completeness result. Loop semantics connects it to Quantum Loop Programs, while practical tool boundaries are discussed in Verification Methods and Tools.

Original paper

Mingsheng Ying, Floyd–Hoare Logic for Quantum Programs, ACM Transactions on Programming Languages and Systems 33(6), Article 19, 1–49 (2011), DOI: 10.1145/2049706.2049708. arXiv:0906.4586