Foundations of Quantum Programming

4.2.5 An Illustrative Example: Reasoning about the Grover Algorithm

In the last two Subsections, we developed the proof system qPD for partial correctness and qTD for total correctness of quantum while-programs, and established their soundness and (relative) completeness. The purpose of this Subsection is to show how the proof systems qPD and qTD can actually be used to verify correctness of quantum programs. We consider the Grover quantum search algorithm as an example.

Recall from Subsection 2.3.3 and Section 3.5 the search problem can be stated as follows. The search space consists of N = 2ⁿ elements, indexed by numbers 0,1,…,N − 1. It is assumed that the search problem has exactly L solutions with $1\le L\le \frac{N}{2}$, and we are supplied with an oracle ...