Proof rules for the correctness of quantum programs

We apply the notion of quantum predicate proposed by D’Hondt and Panangaden to analyze a simple language fragment which may describe the quantum part of a future quantum computer in Knill’s architecture. The notion of weakest liberal precondition semantics, introduced by Dijkstra for classical deterministic programs and by McIver and Morgan for probabilistic programs, is generalized to our quantum programs. To help reasoning about the correctness of quantum programs, we extend the proof rules presented by Morgan for classical probabilistic loops to quantum loops. These rules are shown to be complete in the sense that any correct assertion about the quantum loops can be proved using them. Some illustrative examples are also given to demonstrate the practicality of our proof rules.