Some Problems In Quantum Program Verification

The research works of quantum computation are mainly accomplished by phys-ical scientist and computer scientist, the former pay close attention to the physical implementation of quantum computation, and the later are concerned with the theory and implementation of quantum programming language. Verification of pro-gram is a key technique to guarantee the correctness of program. Such as verification based on logical reasoning, the famous is Hoare logical reasoning; model checking is mostly aimed at the finite state program.A outstanding advantage of quantum communication over classical commu-nication is its security. However, it is very difficult to guarantee the correctness of protocols at the stage of design. Since there are some essential differences be-tween quantum system and classical counterpart, such as no cloning of quantum information, the existence of entanglement, etc., thus the classical theory, method and technique are not mostly straightway applicable to quantum software, hence the research of quantum software becomes to be very difficult and fully challenged question for study or discussion.The discussion of termination condition, complexity of time and space are a very important and difficult problem for the investigation of loop program. In fact, the termination of a general quantum loop program is not determined. In this thesis, we mainly address termination condition of quantum program, which is constituted by quantum channel, generalized quantum loop program and nondeter-ministic quantum program, and also study quantum weakest liberal precondition semantics which is helpful to reason about Hoare logic. Our efforts are beneficial supplement and improvement to the verification theory of quantum program.The main contributions in this thesis are listed as follows:(1) In Chapter3, Using the verification method for quantum program and selecting different observable operators, we investigate the termination of quantum program on the single qubit system described by bit flip channel, depolarizing chan-nel, amplitude damping channel and phase damping channel. It has been shown that the conditions of termination of the quantum program described by quantum channels not only depend on the selection of input state, but also it depend on the selection of observable operators.(2) In Chapter4, we discuss the termination (almost termination) of general-ized quantum loop program (for short GQLoop) when GQLoop is described by bit flip channel, depolarizing channel, amplitude damping channel and phase damping channel, respectively. And we also address the conditions of termination (almost termination) of GQLoop when the loop bodies are the embedding of two kinds of GQLoop. It has been shown that the conditions of termination (almost termination) of GQLoop depend on the parameters occuring in the quantum channels. When the loop bodies are a unitary operation on the principle system and the environment under the open quantum system, after implementing unitary operation, the com-puted process of the quantum program is discussed by performing a partial trace over the environment.(3) In Chapter5, firstly, we discuss the reachable and diverging sets and the termination of a deterministic quantum program (for short DQP) from computa-tional basis states described by bit flip, phase flip, depolarizing, amplitude damping and phase damping channel, respectively, where DQP is a kind of special nondeter-ministic quantum program (for short NDQP). Secondly, we consider detailed the reachable and diverging sets and the termination of an NDQP from computational basis states, where the NDQP consists of two pairs from the above five kinds of channels. It has been shown that the termination condition of an NDQP are better complicated, the termination of some NDQP depends on two parameters depicting quantum channel, however, that of other NDQP does not relate to two parameters depicting quantum channel. Finally, we study the reachable and diverging sets and the termination of an NDQP which is constituted by two quantum walks in C3and C4, respectively. It has been shown that the reachable and diverging sets and the termination of an NDQP are closely connected with measurement operators. An NDQP is possible to terminate or diverge from an initial state under different mea-surement operators; the states of termination and diverging coexist in a reachable set obtained from same initial state.(4) In Chapter6, we propose the definition of quantum weakest liberal pre-condition (for short wlp)wlp (A, B, C)-commutativity, study some necessary and sufficient conditions of wlp (A, B, C)-commutativity. It has been shown that wlp is not a healthy predicate transformer, it is verified that wlp is a weaker predi-cate transformer than quantum weakest precondition (for short wp). We disclose the essential differences of wlp and wp. Finally, we investigate the properties for sequential composition, parallel composition and block structure of wlp, and some properties of&operation.