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.

翻译：精化是计算机程序验证与系统化开发的一项基础技术。它通过逐步精化支持一种严谨的软件构建方法，即一个抽象的规约被逐步转化为满足预期需求的具体实现。该方法论的核心是精化序的概念，它保证每个精化步骤都能保持程序的正确性。本文首次对量子程序的精化序进行了全面研究，涵盖了完全正确性与部分正确性准则下的确定性与非确定性场景。我们研究了量子谓词的三个自然类别：表示定性性质的投影算子；刻画定量性质的效应；以及建模恶魔非确定性的效应集合。对于确定性量子程序，我们证明了基于效应和基于效应集合的规约下的精化，与超算符上的标准完全正定序相一致；而由基于投影算子的规约所诱导的精化，则可以用Kraus算子的线性张成来刻画。对于具有基于效应集合规约的非确定性量子程序，我们建立了与经典域论概念的精确对应：Smyth序刻画了完全正确性下的精化，而Hoare序刻画了部分正确性下的精化。此外，基于效应和基于投影算子的规约会导出严格更弱的精化序。