  Grover's search algorithm is designed to be executed on a quantum mechanical
computer. In this paper, 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 modelling this and other quantum algorithms
and that it also provides a systematic framework of analysing such algorithms.
