This paper presents a refinement calculus designed specifically for quantum programs, offering a structured approach to their progressive and modular development while ensuring correctness throughout the refinement process. We begin by investigating the partial correctness of nondeterministic programs within a quantum while language featuring prescription statements. Orthogonal projectors, which are in one-to-one correspondence to subspaces of the state Hilbert space, are taken as assertions for quantum states. We provide the weakest liberal precondition and strongest postcondition semantics of quantum programs, and based on these dual semantics, introduce refinement rules that facilitate the incremental development of quantum programs. All these rules, as well as their soundness and completeness, are formalized and proven in the Coq proof assistant by utilizing CoqQ, a general-purpose framework for quantum computing and program verification. To demonstrate the utility of the refinement calculus, we examine examples including the implementation of a Z -rotation gate, the repetition error-correction code, and the quantum-to-quantum Bernoulli factory. Moreover, we present QRefine, a Python-based interactive prototype designed as a proof of concept to demonstrate the potential of our approach in the stepwise development of correct quantum programs
Feng et al. (Wed,) studied this question.