Refinement Orders for Quantum Programs

Refinement is a fundamental technique in the verification and systematic development of computer programs. It supports a disciplined approach to software construction through stepwise refinement, whereby an abstract specification is gradually transformed into a concrete implementation that satisfies the desired requirements. Central to this methodology is the notion of a refinement order, which guarantees that each refinement step preserves program correctness. This paper presents the first comprehensive study of refinement orders for quantum programs, covering both deterministic and nondeterministic settings under total and partial correctness criteria. We investigate three natural classes of quantum predicates: projectors, representing qualitative properties; effects, capturing quantitative properties; and sets of effects, modeling demonic nondeterminism. For deterministic quantum programs, we show that refinement with respect to effect-based and set-of-effects based specifications coincides with the standard complete-positivity order on superoperators, whereas refinement induced by projector-based specifications can be characterized by the linear span of Kraus operators. For nondeterministic quantum programs with set-of-effects based specifications, we establish precise correspondences with classical domain-theoretic notions: the Smyth order characterizes refinement under total correctness, while the Hoare order characterizes refinement under partial correctness. Moreover, effect-based and projector-based specifications lead to strictly weaker refinement orders. From a theoretical perspective, our results provide a solid semantic foundation for the development of quantum refinement calculi. From a practical standpoint, they offer concrete guidance for quantum program designers in selecting appropriate predicate classes and correctness notions to support their intended refinement goals.