  Refinement calculus provides a structured framework for the progressive and
modular development of programs, ensuring their correctness throughout the
refinement process. This paper introduces a refinement calculus tailored for
quantum programs. To this end, we first study the partial correctness of
nondeterministic programs within a quantum while language featuring
prescription statements. Orthogonal projectors, which are equivalent to
subspaces of the state Hilbert space, are taken as assertions for quantum
states. In addition to the denotational semantics where a nondeterministic
program is associated with a set of trace-nonincreasing super-operators, we
also present their semantics in transforming a postcondition to the weakest
liberal postconditions and, conversely, transforming a precondition to the
strongest postconditions. Subsequently, refinement rules are introduced based
on these dual semantics, offering a systematic approach to the incremental
development of quantum programs applicable in various contexts. To illustrate
the practical application of the refinement calculus, we examine examples such
as the implementation of a $Z$-rotation gate, the repetition code, and the
quantum-to-quantum Bernoulli factory. Furthermore, we present Quire, a
Python-based interactive prototype tool that provides practical support to
programmers engaged in the stepwise development of correct quantum programs.
