arXiv:2405.01940

On the Relative Completeness of Satisfaction-based Quantum Hoare Logic

Sun, Xin, Xingchi Su, Xiaoning Bian, Huiwen Wu

Published May 3, 2024• 0 citations

Abstract

Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation.

DOI: 10.48550/arxiv.2405.01940

Related papers

Weakest precondition calculus and relative completeness of satisfaction-based quantum Hoare logic

Xin Sun, Xingchi Su, Xiaoning Bian +1 more

Abstract Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with a while loop since its inception in 2006. This paper presents a solution. We prove the relative completeness in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus.

Quantum Information ProcessingJul 28, 20260 citations

Hoare Logic for Quantum Programs

Mingsheng Ying

Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.

arXiv:0906.4586Jun 25, 20099 citations

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic

Junyi Liu, Bohua Zhan, Shuling Wang +5 more

We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.

Lecture notes in computer scienceJan 1, 201983 citations

Formal Verification of Continuous-Variable Quantum Programs

Stefanie Muroya, Thomas A. Henzinger

We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.

quant-pharXiv:2607.17714Jul 21, 20260 citations

Quantum Hoare Logic with Classical Variables

Yuan Feng, Mingsheng Ying

Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this article, we propose a quantum Hoare logic for a simple while language that involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided that support standard logical operation in the classical part of assertions and super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor’s factorisation, are formally verified to show the effectiveness of the logic.

arXiv:2008.06812ACM Transactions on Quantum ComputingDec 21, 202144 citations

A Theorem Prover for Quantum Hoare Logic and Its Applications

Tao Liu, Yangjia Li, Shuling Wang +2 more

Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices. Due to the limitation of Isabelle/HOL, the calculation of the order relation is solved by calling an outside oracle written in Python. To the best of our knowledge, this is the first theorem prover for quantum programs. To demonstrate its power, the correctness of two well-known quantum algorithms, i.e., Grover Quantum Search and Quantum Phase Estimation (the key step in Shor's quantum algorithm of factoring in polynomial time) are proved using the theorem prover. These are the first mechanized proofs for both of them.

arXiv:1601.03835Jan 15, 201617 citations