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.

翻译：精化演算为程序的渐进式模块化开发提供了结构化框架，确保其在精化过程中始终正确。本文提出了一种专为量子程序设计的精化演算。为此，我们首先研究包含处方陈述的量子while语言中非确定性程序的部分正确性。选取与状态希尔伯特空间子空间等价的正交投影算子作为量子状态的断言。除了将非确定性程序关联为迹非增超算符集合的指称语义外，我们还呈现了其将后条件变换为最弱自由后条件，以及将前条件变换为最强后条件的语义。随后，基于这些对偶语义引入精化规则，为不同场景下量子程序的增量开发提供系统化方法。为说明精化演算的实际应用，我们考察了Z旋转门实现、重复码以及量子到量子伯努利工厂等实例。此外，我们提出Quire——一款基于Python的交互式原型工具，为从事正确量子程序逐步开发的程序员提供实用支持。