Hoare Logic for Quantum Programs

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.


Introduction
Even though quantum hardware is still in its infancy, people widely believe that building a large-scale and functional quantum computer is merely a matter of time and concentrated effort. The history of classical computing arouses that once quantum computers come into being, quantum programming languages and quantum software development techniques will play a key role in exploiting the power of quantum computers. With expectation of offering effective programming techniques for quantum computers, several quantum programming languages have already been designed in recent years. The earliest proposal for quantum programming language was made by Knill [13]. The first real quantum programming language, QCL, was proposed byÖmer [16]; he also implemented a simulator for this language. A quantum programming language in the style of Dijkstra's guarded-command language, qGCL, was presented by Sanders and Zuliani [18]. A quantum extension of C++ was proposed by Bettelli et al [6], and it was implemented in the form of a C++ library. The first and very influential quantum language of the functional programming paradigm, QFC, was defined by Selinger [19] based on the idea of classical control and quantum data. In [2], Altenkirch and Grattage defined another functional programming language for quantum computing, QML, in which both control and data may be quantum. For excellent survey of quantum programming languages, see [20,12].
The fact that human intuition is much better adapted to the classical world than the quantum world is one of the major reasons that it is difficult to find efficient quantum algorithms. It also implies that programmers will commit much more faults in designing programs for quantum computers than programming classical computers. Thus, it is even more critical than in classical computing to give clear and formal semantics to quantum programming languages and to provide formal methods for reasoning about quantum programs. Indeed, various semantic approaches to quantum programs have been proposed in recent literatures. For example, an operational semantics was given to Sanders and Zuliani's language qGCL [18] by treating an observation (quantum measurement) procedure as a probabilistic choice; a denotational semantics was defined for Selinger's language QPL [19] by interpreting quantum programs as super-operators; and a denotational semantics of Altenkirch and Grattage's language QML [2] was described in category-theoretic terms. In addition, a language-independent approach to semantics of quantum programs was proposed by D'Hondt and Panangaden [10] who introduced an intrinsic notion of quantum weakest precondition and established a beautiful Stone-type duality between state transition semantics and predicate transformer semantics for quantum programs.
As to proof systems for reasoning about quantum programs, Baltag and Smets [4,5,1] presented a dynamic logic formalism of information flows in quantum systems, which is capable of describing various quantum operations such as unitary evolutions and quantum measurements, and particularly entanglements in multi-partite quantum systems. Brunet and Jorrand [8] introduced a way of applying Birkhoff and von Neumann's quantum logic [7] to the study of quantum programs by expanding the usual propositional languages with new primitives representing unitary transformations and quantum measurements. In [9], Chadha, Mateus and Sernadas proposed a Hoare-style proof system for reasoning about imperative quantum programs using a quantitative state logic, but only bounded iterations are allowed in their programming language. Feng et al [11] found some useful proof rules for reasoning about quantum loops, generalizing some of Morgan's proof rules for probabilistic loops [14]. To the author's best knowledge, however, no complete Hoare logic for quantum programs has been reported in the literature.
The main contribution of the present paper is the establishment of a full-fledged Hoare logic for deterministic quantum programs based on Selinger's idea of modeling quantum programs as super-operators and D'Hondt and Panangaden's notion of quantum predicate as an Hermitian operator [10]. This logic includes a proof system for partial correctness and a proof system for total correctness of deterministic quantum programs. In particular, we are able to prove its (relative) completeness by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs. The paper is organized as follows: For convenience of the reader, we recall some basic concepts of Hilbert spaces as well as the fundamental postulates of quantum mechanics in Section 2. Another aim of Section 2 is to fix notation used in the sequel sections. In Section 3, we define the syntax of deterministic quantum programs about which the Hoare logic presented in this paper is designed to reason. Such quantum programs are quantum extension of classical while-programs (cf. [3], Chapter 3). In Section 4, an operational semantics of quantum programs is given in terms of transitions between quantum configurations, which consist of a quantum program still to be executed and a (partial) density operator expressing the current state of program variables. In Section 5, we are able to introduce a denotational semantics of quantum programs based on the operational semantics. A denotational semantics of a quantum program is defined to be a function from partial density operators to themselves. In Section 6, we adopt D'Hondt and Panangaden's definition of quantum predicates as Hermitian operators. Then a correctness formula is defined to be a quantum extension of Hoare triple, which consists of two quantum predicates, namely precondition and postcondition, as well as a quantum program. Furthermore, the notions of partial and total correctness can be introduced for quantum programs using their denotational semantics. In Section 7, weakest precondition and weakest liberal precondition for quantum programs are defined in terms of total and partial correctness, respectively, in a familiar way. With the long preparation of the previous sections, the Hoare logic for quantum programs is finally established in Sections 8 and 9. In Section 8, a proof system for partial correctness of quantum programs is presented, and its (relative) completeness is proved, and in Section 9, after introducing the notion of bound function for quantum loops, a proof system for total correctness of quantum programs is given, and its (relative) completeness is also proved. A brief conclusion is drawn and some open problems for further studies are pointed out in Section 10.
For any vector |ψ in H, its length ||ψ|| is defined to be ψ|ψ . A vector |ψ is called a unit vector if ||ψ|| = 1. Let {|ψ n } be a sequence of vectors in H and |ψ ∈ H. If for any ǫ > 0, there exists a positive integer N such that ||ψ m − ψ n || < ǫ for all m, n ≥ N , then {|ψ n } is called a Cauchy sequence. If for any ǫ > 0, there exists a positive integer N such that ||ψ n − ψ|| < ǫ for all n ≥ N , then |ψ is called a limit of {|ψ n } and we write |ψ = lim n→∞ |ψ n .
A family {|ψ i } i∈I of vectors in H is said to be summable with the sum |ψ and we write |ψ = i∈I |ψ i if for any ǫ > 0 there is a finite subset J of I such that ||ψ − i∈K ψ i || < ǫ for every finite subset K of I containing J. A family {|ψ i } i∈I of unit vectors is called an orthonormal basis of H if 1. |ψ i ⊥ |ψ j for any i, j ∈ I with i = j; and 2. |ψ = i∈I ψ i |ψ |ψ i for each |ψ ∈ H.
In this case, the cardinality of I is called the dimension of H.
A Hilbert space is defined to be a complete inner product space; that is, an inner product space in which each Cauchy sequence of vectors has a limit. According to a basic postulate of quantum mechanics, the state space of an isolated quantum system is represented by a Hilbert space, and a pure state of the system is described by a unit vector in its state space.
The inner product in H 2 is defined by An operator A on H is said to be bounded if there is a constant C ≥ 0 such that A|ψ ≤ C · ψ for all |ψ ∈ H. In this paper, we only consider bounded operators. We write L(H) for the set of bounded operators on H. A density operator ρ on a Hilbert space H is defined to be a positive operator with tr(ρ) = 1. Then a mixed state of a quantum system with state space H is described by a density operator on H. In this paper, we take a slightly generalized notion of density operator in the sequel: a partial density operator ρ is a positive with tr(ρ) ≤ 1. In particular, the zero operator is a partial density operator. The set of partial density operators is denoted D − (H). A partial density operator can also be defined by an ensemble of pure states. Suppose that a quantum system is in one of a number of pure states |ψ i , with respective probabilities p i , where it is required that i p i ≤ 1. Then is a density operator. Conversely, any density operator can be generated in such a way.

Unitary Transformations
and the Pauli matrices: 2. Let k be an integer. Then the k−translation operator on H ∞ is defined by It is easy to verify that U +k is a unitary operator.
The basic postulate of quantum mechanics about evolution of systems may be stated as follows: Suppose that the states of a closed quantum system at times t 0 and t are |ψ 0 and |ψ , respectively. Then they are related to each other by a unitary operator U which depends only on the times t 0 and t, This postulate can be reformulated in the language of density operators as follows: The state ρ of a closed quantum system at time t is related to its state ρ 0 at time t 0 by a unitary operator U which depends only on the times t and t 0 ,

Quantum Measurements
A quantum measurement on a system with state space H is described by a collection where M m are called measurement operators, and the index m stands for the measurement outcomes that may occur in the experiment. If the state of a quantum system is |ψ immediately before the measurement, then the probability that result m occurs is p(m) = ψ|M † m M m |ψ and the state of the system after the measurement is We can also formulate the quantum measurement postulate in the language of density operators. If the state of a quantum system was ρ immediately before measurement {M m } is performed on it, then the probability that result m occur is and the state of the system after the measurement is A special class of quantum measurements will be frequently used in the sequel: If a measurement M has only two outcomes, say 0 and 1; that is, M = {M 0 , M 1 }, then we often call M a yes-no measurement, with 0 corresponding to "no"and 1 to "yes".

Tensor Products of Hilbert Spaces
The state space of a composite quantum system is the tensor product of the state spaces of its components. In this subsection, we recall the definition of the tensor product of a family {H i } of Hilbert spaces. For simplicity of presentation, it will be assumed that the set of quantum variables is countably infinite, and the type of each quantum variable is either Boolean or integer (see next section). Thus, we only need to consider a finite or countably infinite family {H i } where each H i is finite-dimensional or countably infinite-dimensional. A more general notion of tensor product introduced by von Neumann [21] should be adopted in order to generalize the results obtained in this paper to the case of more quantum variables and other types.
Let {|ψ ij i } be an orthonormal basis of H i for each i. We write B for the set of tensor products of basis vectors of all H i ; that is, Then B is a countably infinite set, and it can be written in the form of a sequence of vectors: B = {|ϕ n : n = 0, 1, ...}.
The tensor product of {H i } is defined to be the Hilbert space spanned by B, i.e.
We define the inner product in i H i as follows: ( n α n |ψ n , n α ′ n |ψ n ) = n α * n α ′ n for any α n , α ′ n ∈ C, n ≥ 0. It is easy to see that i H i is isomorphic to H ∞ . The notion of partial trace is very useful for description of a subsystem of a composite quantum system. Let H and K be two Hilbert spaces and operator A ∈ L(H ⊗ K). Then the partial trace of A on H is defined to be which is an operator on H, where {|ψ i } is an orthonormal basis of K. It can be shown that tr K (A) does not depend on choice of {|ψ i }. In particular, if H 1 and H 2 are the state spaces of quantum systems q 1 and q 2 , respectively, and the state of their composite system q 1 q 2 is described by a density operator ρ ∈ D − (H 1 ⊗ H 2 ), then tr H 2 (ρ) is the description for the state of component system q 1 .

Syntax of Quantum Programs
We assume a countably infinite set V ar of quantum variables. The symbols q, q ′ , q ′′ , q 0 , q 1 , q 2 , ... will be used as meta-variables ranging over quantum variables. Recall that in classical computation, we use a type to denote the domain of a variable. Thus, in quantum computation, a type should be the state space of a quantum system denoted by some quantum variable. Formally, a type t is a name of a Hilbert space H t . In this paper, we only consider two basic types: Boolean, integer. The results obtained in this paper can be easily generalized to the case with more types. The Hilbert spaces denoted by Boolean and integer are: Note that the sets denoted by types Boolean and integer in classical computation are exactly the computational bases of H Boolean and H integer , respectively (see Example 2.1). Now we assume that each quantum variable q has a type type(q), which is either Boolean or integer. The state space H q of a quantum variable q is the Hilbert space denoted by its type; that is, A quantum register is defined to be a finite sequence of distinct quantum variables. The state space of a quantum register q = q 1 , ..., q n is the tensor product of the state spaces of the quantum variables occurring in q; that is, Now we are able to define the syntax of quantum programs. The quantum programs considered in this paper are quantum extension of classical while-programs. Formally, they are generated by the following grammar: where • q is a quantum variable and q a quantum register; • U in the statement "q := U q"is a unitary operator on H q . In particular, if type(q) = integer, then the statement q := U +k q, where U +k is the k−translation operator, will be often abbreviated to q := q + k; • in the statement "measure M [q] : S", M = {M m } is a measurement on the state space H q of q, and S = {S m } is a set of quantum programs such that each outcome m of measurement M corresponds to S m ; The intuitive meaning of these quantum program constructs will become clear after introducing their operational semantics in the next section.
The following technical definition will be needed in the sequel.

Operational Semantics of Quantum Programs
We write H all for the tensor product of the state spaces of all quantum variables, that is, For simplicity of presentation, we will use E to denote the empty program. A quantum configuration is a pair S, ρ , where S is a quantum program or E, ρ ∈ D − (H all ) is a partial density operator on H all , and it is used to indicate the (global) state of quantum variables. Let q = q 1 , ..., q n be a quantum register. A linear operator A on H q has a cylinder extension on H all , where I V ar−{q} is the identity operator on the Hilbert space In the sequel, we will simply for A for its extension (1), and it can be easily recognized from the context, without any risk of confusion. The operational semantics of quantum program is defined to be a transition relation → between quantum configurations. By a transition S, ρ → S ′ , ρ ′ we mean that after executing quantum program S one step in state ρ, the state of quantum variables becomes ρ ′ , and S ′ is the remainder of S still to be executed. In particular, if S ′ = E, then S terminates in state ρ ′ . The transition relation → is given by the transition rules in Fig.1.
The meanings of various program constructs are precisely specified by the transitional rules in Fig.1. The statement "skip"does nothing and terminates immediately. The initialization "q := 0"sets quantum variable q to the basis state |0 . To see the role of initialization more clearly, we consider the case of type(q) = integer as an example. First, suppose ρ is a pure state; that is, ρ = |ψ ψ| for some |ψ ∈ H all . We can write |ψ in the form: where |ψ k is a product state, say After the initialization the state becomes: In general, suppose ρ is generated by an ensemble {(p i , |ψ i )} of pure states, that is, For each i, we write ρ i = |ψ i ψ i | and assume that it becomes ρ q i0 after the initialization. By the above argument, we can write ρ i0 in the form: where |ϕ ik ∈ H var−{q} for all k. Then the initialization makes that ρ becomes From Eqs. (2) and (3) we see that the state of q is set to be |0 and the states of the other quantum variables are unchanged. The statement "q := U q"simply means that unitary transformation U is performed on quantum register q, leaving the states of the quantum variables not in q unchanged. Remark that U in the target configuration of the rule (Unitary Transformation) stands indeed for the cylinder extension of U on H all (see Eq. (1)). A similar remark applies to the rules for measurements and loops. Sequential composition is similar to its counterpart in classical computation. The program construct "measure M [q] : S"is a quantum generalization of classical conditional statement. Recall that the first step of the execution of conditional statement "if B then S 1 else S 2 fi"is to check whether Boolean expression B is satisfied. However, according to a basic postulate of quantum mechanics, the unique way to acquire information about a quantum system is to perform a measurement on it. So, in executing the statement "measure M [q] : S", quantum measurement M will first be performed on quantum register q, and then a subprogram S m in S will be selected to be executed next according to the outcome of measurement. The essential difference between a measurement statement and a classical conditional statement is that the state of program variables is changed after performing the measurement in the former, whereas it is not changed after checking the Boolean expression in the latter. Note that the outcome m is observed with probability and after the measurement the state becomes So, a natural presentation of the Measurement rule is the probabilistic transition: However, we adopt Selinger's suggestion [19] of encoding both probability p m and density operator ρ m into partial density operator This allows us to give the Measurement rule in terms of ordinary transition. The statement "while M [q] = 1 do S"is a quantum generalization of classical loop "while B do S od". To acquire information about quantum register q, a measurement M is performed on it. The measurement M is a yes-no measurement with only two possible outcomes 0, 1. If the outcome 0 (no) is observed, then the program terminates, and if the outcome 1 (yes) occurs, then the program executes the subprogram S and continues. The only difference between a quantum loop and a classical loop is that checking the loop guard B in a classical loop does not change the state of program variables, but in a quantum loop the measurement outcomes 0 and 1 occur with probabilities: respectively, and the state becomes M 0 ρM † 0 from ρ when the outcome is 0, and it becomes M 1 ρM † 1 when the outcome is 1. Again, we adopt Selinger's suggestion so that the (Loop 0) and (Loop 1) rules can be stated as ordinary transitions instead of probabilistic transitions.
Let S be a quantum program and ρ ∈ D − (H). If S ′ , ρ ′ can be reached from S, ρ in n steps in the transition relation →; that is, there are configurations S 1 , ρ 1 , ..., S n−1 , ρ n−1 such that A transition sequence of S starting in ρ is a finite or infinite sequence of configurations in the following form: If it cannot be extended, then it is called a computation of S starting in ρ. Moveover, if it is finite and its last configuration is E, ρ ′ , then we say that it terminates in ρ ′ ; and if it is infinite, then we say that it diverges. We say that S can diverge from ρ whenever it has a diverging computation starting in ρ.
Classical while-programs are a typical class of deterministic programs that have exactly one computation starting in a given state. As shown in the following example, however, quantum while-programs no longer possess such a determinism because probabilism is introduced by the measurements in the statements "measure M [q] : S"and "while M [q] = 1 do S". After encoding probabilities into partial density operators, probabilism manifests as nondeterminism in transition rules (Measurement), (Loop 0) and (Loop 2).
Example 4.1 Suppose that type(q 1 ) = Boolean and type(q 2 ) = integer. Consider the program: Then the computations of S starting in ρ are: S, ρ → q 2 := 0; q 1 := Hq 1 ; q 2 := q 2 + 2; measure, ρ 1 → q 1 := Hq 1 ; q 2 := q 2 + 2; measure, ρ 2 where measure stands for the statement "measure M [q 1 ] : S", and So, S can diverge from ρ. Note that S 2 has also the transition but we always discard the transitions in which the partial density operator of the target configuration is zero operator.

Denotational Semantics of Quantum Programs
The denotational semantics of a quantum program is defined to be a semantic function which maps partial density operators to themselves. More precisely, for any quantum program S, the semantic function of S sums the computated results of all terminating computations of S. We write → * for the reflexive and transitive closures of →; that is, S, ρ → * S ′ , ρ ′ if and only if S, ρ → n S ′ , ρ ′ for some n ≥ 0.
Definition 5.1 Let S be a quantum program. Then its semantic function It should be pointed out that {| · |} in Eq. (4) stands for multi-set. The reason for using multi-sets is that the same density operator may be obtained through different computational paths as we can see from the measurement and loop rules in the operational semantics. The following simple example illustrates the case more explicitly. • S = S 0 , S 1 , S 0 = q := Iq and S 1 = q := σ x q.
Then the computation of S starting in ρ is given as follows: where measure is an abbreviation of "measure M [q] : S". So, we have: Now we are going to establish some basic properties of semantic functions. First, we prove its linearity.
, then for any quantum program S, we have: Proof. We can easily prove the following fact by induction on the structure of S: Then the conclusion immediately follows. Next we give a representation of semantic function [|S|] according to the structure of program S. To do this for quantum loops, we need some auxiliary notations. Let Ω be a quantum program such that [|Ω|] = 0 H all for all ρ ∈ D(H); for example, where q is a quantum variable, and is a trivial measurement on H q . We set: and if type(q) = integer, then Proof. (1), (2) and (3) are obvious.
(4) By Lemma 5.1 and the transitional rule for sequential composition we obtain: (5) follows immediately from the transitional rule for measurement.
(6) We introduce two auxiliary operators: for all ρ ∈ D − (H) and i = 0, 1. For simplicity, we write while for "while M [q] = 1 do S". First, we prove: for all n ≥ 1 by induction on n. The case of n = 1 is obvious. Then by (1), (4) and (5) and the induction hypothesis on n − 1 we obtain: Second, we have: So, it suffices to show that for all n ≥ 1. This can be easily done by induction on n.
If we only consider quantum variables of type Boolean, then the above proposition coincides with Fig.1 in [11]. However, it is worth noting that in [11] the denotational semantics of quantum programs was directly defined and it lacks a basis of operational semantics. Similar to Lemma 3.2 in [11], we may prove that the semantic function of a quantum program is a super-operator. Thus, the denotational semantics given in this section is consistent with Selinger's idea of modeling quantum programs as super-operators [19].
A recursive characterization of the semantic function of a quantum loop can be derived from the above proposition. Proof.Immediate from Proposition 5.1(6) and Eq. (5).
The following proposition shows that a semantic function does not increase the trace of density operator of quantum variables.    for all n ≥ 0. This can be carried out by induction on n. The case of n = 0 is obvious. By the induction hypothesis on n and S ′ , we have: From the proof of the above proposition, it is easy to see that the unique possibility that tr([|S|](ρ)) < tr(ρ) comes from the quantum loops occurring in S. Thus, tr(ρ) − tr([|S|](ρ)) is the probability that program S diverges from input state ρ. This can be further illustrated by the following example. For simplicity, we write while for this program. Let This means that program while terminates on input ρ with probability 1 2 , and it diverges from input ρ with probability 1 2 .
To conclude this section, we observe how quantum programs change the states of quantum variables and how they access quantum variables.
Let X ⊆ V ar be a set of quantum variables. For any A ∈ L(H all ), we write tr X (A) for tr N q∈X Hq (A). We put the long and dumb proof of the above proposition into the appendix.
Recall that tr X (ρ) describes the state of the quantum variables not in X when the global state of all quantum variables is ρ. So, Proposition 5.3 (1) indicates that the state of the quantum variables not in var(S) after implementing quantum program S is the same as that before implementing S. This means that program S can only change the state of quantum variables in var(S). On the other hand, Proposition 5.3 (2) shows that if two input states ρ 1 and ρ 2 coincide on the quantum variables in var(S), then the computed outcomes of S, starting in ρ 1 and ρ 2 , respectively, will also coincide on these quantum variables. In other words, program S can access at most the quantum variables in var(S).

Correctness Formulas
Correctness of a quantum program will be expressed by a quantum extension of Hoare triple in which a quantum predicate describes the input state and a quantum predicate describes the output states of the program. We adopt D'Hondt and Panangaden's definition of quantum predicates [10]. For any X ⊆ V ar, a quantum predicate on H X is defined to be a Hermitian operator P on H X such that We write P(H X ) for the set of quantum predicates on H X . Intuitively, for any ρ ∈ D − (H X ), tr(P ρ) stands for the probability that predicate P is satisfied in state ρ.
A correctness formula is a statement of the form:

{P }S{Q}
where S is a quantum program, and both P and Q are quantum predicates on H all . The quantum predicate P is called the precondition of the correctness formula and Q the postcondition. A correctness formula can be interpreted in two different ways: for all ρ ∈ D − (H).
The intuitive meaning of the defining inequality of total correctness is: the probability that input ρ satisfies quantum predicate P is not greater than the probability that quantum program S terminates on ρ and its output [|S|](ρ) satisfies quantum predicate Q. Recall that tr(ρ)−tr([|S|](ρ)) is the probability that quantum program S diverges from input ρ. Thus, the definition inequality of partial correctness means: if input ρ satisfies predicate P , then either program S terminates on it and its output [|S|](ρ) satisfies Q, or S diverges from it. The difference between total correctness and partial correctness is illustrated well by the following simple example.

Then it follows from linearity of [|S|] (Lemma 5.1) that
for all ρ ∈ D − (H all ).
Proof. Immediate from definition.

Weakest Preconditions and Weakest Liberal Preconditions
As in the case of classical Hoare logic, the notions of weakest precondition and weakest liberal precondition of quantum program will play a key role in establishing the (relative) completeness of Hoare logic for quantum programs. They may be defined in a familiar way: The next two propositions give explicit representations of weakest preconditions and weakest liberal preconditions, respectively. They will be used in the proof of completeness of quantum Hoare logic.
Proof. The trick is to simultaneously prove (1) and (2) by induction on the structure. This is indeed why we put these two conclusions that seem irrelevant at the first glance into a single proposition. Case 1. S = skip. Obvious. Case 2. S = q := 0. We only consider the case of type(q) = integer, and the case of type(q) = Boolean is similar. First, it holds that tr((  This claim can be proved by induction on n. The basis case of n = 0 is obvious. By the induction hypotheses on n and S ′ , we obtain: Proof. Similar to the case of weakest precondition, we prove (1) and (2) by induction on n, where (while) n is an abbreviation of (while M [q] = 1 do S ′ ) n . The case of n = 0 is obvious. By induction on S ′ and induction hypothesis on n, we observe: This completes the proof of Eq. (6). Note that quantum predicate P ⊑ I. Then I − P is positive, and by continuity of trace operator we obtain: For any Q ∈ P(H all ), |= par {Q}S{P } implies: for all ρ ∈ D − (H all ). This together with Lemma 2.1 leads to Q ⊑ ∞ n=0 P n . We see that Propositions 7.1 and 7.2 coincide with Figs. 2 and 3, respectively, in [11] when only quantum variables of type Boolean are considered. But Figs. 2 and 3 in [11] are given directly as definitions, and their intuitive meanings are not clear because they do not have any connection to total and partial correctness of quantum programs. In contrast, Propositions 7.1 and 7.2 fill in such a gap, and they are derived from Definition 7.1, which is given entirely based on the notions of total and partial correctness of quantum programs.
The next proposition gives a recursive characterization of weakest precondition and weakest liberal precondition of quantum loop, and it provides a key step in the proof of completeness of quantum Hoare logic. Proof. We only prove (2), and the proof of (1) is similar and easier. For every ρ ∈ D − (H all ), by Proposition 7.2(2) we observe:

Proof System for Partial Correctness
Now we are ready to present an axiomatic system of Hoare logic for quantum programs. The quantum Hoare logic can be divided into two proof systems, one for partial correctness and one for total correctness. In this section, we introduce the proof system qP D for partial correctness of quantum programs. It consists of the axioms and inference rules in Fig. 2.
We first prove the soundness of the proof system qP D with respect to the semantics of partial correctness: provability of a correctness formula in qP D implies its truth in the sense of partial correctness.
Theorem 8.1 (Soundness) The proof system qP D is sound for partial correctness of quantum programs; that is, for any quantum program S and quantum predicates P, Q ∈ P(H all ), we have: Proof. We only need to show that the axioms and inference rules of qP D are valid in the sense of partial correctness.
(Axiom Initialization) We only prove the case of type(q) = integer, and the case of type(q) = Boolean is similar. For any ρ ∈ D − (H all ), it follows from Proposition 5.1.2 that = tr(P [|q := 0|](ρ)). Therefore, we have: Furthermore, we have: for all n ≥ 1. In fact, Eq. (8) may be proved by induction on n. The case of n = 1 is obvious. Using Eq. (7), we obtain: Combining Eqs. (8) and (9), we assert that Therefore, Eq. (8) holds in the case of n + 1 provided it is true in the case of n, and we complete the proof of Eq. (8). Now we note that Then it follows that On the other hand, we have: Putting Eqs. (10) and (11) into Eq. (8), we obtain: Let n → ∞. Then it follows that and Now we are going to establish completeness for the proof system qP D with respect to the semantics of partial correctness: truth of a quantum program in the sense of partial correctness implies its provability in qP D. Note that the Löwner ordering assertions between quantum predicates in (Rule Order) are statements about complex numbers. So, only a completeness of qP D relative to the theory of the field of complex numbers may be anticipated; more precisely, we can add all statements that are true in the field of complex numbers into qP D in order to make it complete. The following theorem should be understood exactly in the sense of such a relative completeness. Theorem 8.2 (Completeness) The proof system qP D is complete for partial correctness of quantum programs; that is, for any quantum program S and quantum predicates P, Q ∈ P(H all ), we have: Proof. If |= par {P }S{Q}, then by Definition 7.1 (2) we have P ⊑ wlp.S.Q. Therefore, by (Rule Order) it suffices to prove the following: We proceed by induction on the structure of S. Case 1. S = skip. Immediate from (Axiom Skip). Case 2. S = q := 0. Immediate from (Axiom Initialization).

Proof System for Total Correctness
The aim of this section is to present a proof system qT D for correctness of quantum program. The only difference between qT D and qP D is the inference rule for quantum loops. To give the rule for total correctness of quantum loops, we need a notion of bound function which express the number of iterations of a quantum loop in its computation.
Recall that a bound function t of a classical loop "while B do S od "satisfies the inequality t([|S|](s)) < t(s) for any input state s. It is interesting to compare it with conditions (1) and (2) of the above definition, and we see that the latter are two inequalities between t([|S|](M 1 ρM † 1 )) and t(ρ) but not between t([|S|](ρ)) and t(ρ). This is because in the implementation of the quantum loop "while M [q] = 1 do S", we need to perform the yes-no measurement M on ρ when checking the loop guard "M [q] = 1", and the state of quantum variables will become M 1 ρM † 1 from ρ whence the measurement outcome "yes"is observed.
The following lemma gives a characterization of the existence of bound function of a quantum loop in terms of the limit of the state of quantum variables when the number of iterations of the loop goes to infinity. It provides a key step for the proof of soundness and completeness of the proof system qT D. Then it holds that tr(P ρ k ) ≥ ǫ 0 , and by conditions 1 and 2 in Definition 9.1 we obtain: Consequently, we have an infinitely descending chain {t ǫ 0 (ρ k )} in N, the set of nonnegative integers. This is a contradiction because N is a well-founded set. ( then for any ǫ > 0, there exists N ∈ N such that tr(P ([|S|] • E 1 ) n (ρ)) < ǫ for all n ≥ N . We define: Now it suffices to show that t ǫ is a (P, ǫ)−bound function of loop "while M [q] = 1 do S". To this end. we consider the following two cases: Case 1. tr(P ρ) ≥ ǫ. Suppose that t ǫ (ρ) = N . Then tr(P ρ) ≥ ǫ implies N ≥ 1. By the definition of t ǫ , we assert that Therefore, t ǫ ([|S|](M † 1 ρM 1 )) ≤ N − 1 < N = t ǫ (ρ). Case 2. tr(P ρ) < ǫ. Again, suppose that t ǫ (ρ) = N . Now we have the following two subcases: Subcase 2.1. N = 0. Then for all n ≥ 0, It is easy to see that t ǫ ([|S|](M 1 ρM † 1 )) = 0 = t ǫ (ρ). Subcase 2.2. n ≥ 1. We can derive that in the way of Case 1. Now we are ready to present the proof system qT D for total correctness of quantum programs. It consists of the axioms (Axiom Skip), (Axiom Initialization) and (Axiom Unitary Transformation) and inference rules (Rule Sequential Composition), (Rule Measurement) and (Rule Order) in Fig.2 as well as inference rule (Rule Loop Total) in Fig.3.
The remainder of this section will be devoted to establish soundness and completeness of qT D: provability of a correctness formula in qT D is equivalent to its truth in the sense of total correctness. Theorem 9.1 (Soundness) The proof system T D is sound for total correctness of quantum programs; that is, for any quantum program S and quantum predicates P, Q ∈ P(H all ), we have: Proof. It suffices to show that the axioms and inference rules of T D are valid in the sense of total correctness.
The proof for soundness of (Axiom Skip), (Axiom Initialization) and (Axiom Unitary Transformation) is similar to the case of partial correctness. ( We first prove the following inequality: by induction on n. It holds that So, Eq. (13) is correct for the base case of n = 0. Assume Eq. (13) is correct for the case of n = m. Then applying Eq. (12), we obtain: Therefore, Eq. (13) also holds for the case of n = M + 1. Now, since for any ǫ > 0, there exists M † 1 QM 1 , ǫ−bound function t ǫ of quantum loop "while M [q] = 1 do S", by Lemma 9.1 we have: = tr(P [|while M [q] = 1 do S|](ρ)).
Theorem 9.2 (Completeness) The proof system T D is complete for total correctness of quantum programs; that is, for any quantum program S and quantum predicates P, Q ∈ P(H all ), we have: Proof. Similar to the case of partial correctness, it suffices to prove the following: So, our aim is to derive that By the induction hypothesis on S ′ we get: First, by Propositions 7.1 (2) and 5.1 (6) we observe: Second, we consider the following infinite series of nonnegative real numbers: Since Q ⊑ I H all , it follows from Propositions 5.1 (6) and 5.2 that Therefore, the infinite series Eq. (16) (14), and we complete the proof.
It should be pointed out that the above theorem is merely a relative completeness of qT D with respect to the theory of the fields of complex numbers because except that (Rule Order) is employed in qT D, the existence of bound functions in (Rule Loop Total) is also a statement about complex numbers.

Conclusion
Based on D'Hondt and Panangaden's idea of representing quantum predicates by Hermitian operators and Selinger's idea of modeling quantum programs by superoperators, a full-fledged Hoare logic is developed for deterministic quantum programs, and its completeness relative to the theory of the field of complex numbers is proved in this paper.
An interesting problem for further studies is to find reasonable extensions of the quantum Hoare logic presented in this paper for bigger classes of quantum programs, including nondeterministic quantum programs [25], parallel and distributed quantum programs. Hopefully, they will serve as a logical foundation of various effective techniques for verification of these bigger classes of quantum programs.
Appendix: Proof of Proposition 5.3 (1) We proceed by induction on the structure of S. Case 1. S = skip. Obvious. Case 2. S = q := 0. We only consider the case of type(q) = integer, and the case of type(q) = Boolean is similar. It holds that Case 3. S = q := U q. If {|ψ i } is an orthonormal basis of H q , then {U † |ψ i } is also an orthonormal basis of H q . Consequently, = tr var(S) (ρ).