Reasoning about Grover's quantum search algorithm using probabilistic wp

Grover's search algorithm is designed to be executed on a quantum-mechanica l computer. In this article, the probabilistic wp-calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus provides a rigorous programming notation for modeling this and other quantu m algorithms and that it also provides a systematic framework of analyzing such algorithms.