A Formal Derivation of Grover´s Quantum Search Algorithm

In this paper we aim at applying established formal methods techniques to a recent software area: quantum programming. In particular, we aim at providing a stepwise derivation of Grover´s quantum search algorithm. Our work shows that, in principle, traditional software engineering techniques such as specification and refinement can be applied to quantum programs. We have chosen Grover´s algorithm as an example because it is one of the two main quantum algorithms. The algorithm can find with high probability an element in an unordered array of length L in just O(radicL) steps (while any classical probabilistic algorithm needs Omega(L) steps). The derivation starts from a rigorous probabilistic specification of the search problem, then we stepwise refine that specification via standard refinement laws and quantum laws, until we arrive at a quantum program. The final program will thus be correct by construction.