© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

arXiv:2504.14158 · ACM Transactions on Software Engineering and Methodology

Refinement Orders for Quantum Programs

Yuan Feng, Li Zhou

Published Aug 25, 2026• 0 citations

Abstract

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.

DOI: 10.1145/3843234

Related papers

Refinement Calculus of Quantum Programs with Projective Assertions

Yuan Feng, Li Zhou, Yingte Xu +1 more

This article 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.

arXiv:2311.14215•ACM Transactions on Software Engineering and Methodology•Oct 1, 2025•3 citations

Verification of Nondeterministic Quantum Programs

Yuan Feng, Yingte Xu

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.

arXiv:2302.07973•International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)•Mar 20, 2023•11 citations

QbC: Quantum Correctness by Construction

Anurudh Peduri, Ina Schaefer, Walter, Michael

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

arXiv:2307.15641•Jul 28, 2023•1 citation

Predicatet transformers for nondeterministic quantum programs

Xi Wang

Nondeterminism has been introduced into quantum programming languages to model, for example, unspecified behavior. Weakest precondition transformers provide a formal framework for reasoning about program correctness with respect to a given postcondition. This thesis combines these ideas by introducing demonic and angelic interpretations of nondeterminism for quantum programs, together with corresponding weakest liberal precondition transformers. To capture angelic nondeterminism in a qualitative setting, we introduce predicates represented by sets of subspaces, where each subspace is represented by a projection. Such a predicate is satisfied whenever the quantum state belongs to one of the represented subspaces. We show, however, that natural definitions of the weakest liberal precondition transformer based on these predicates do not behave as desired for measurements and loops in the demonic setting. For this reason, the demonic weakest liberal precondition transformer is restricted to singleton postconditions. We further investigate the corresponding non-liberal weakest precondition transformers using termination spaces. This yields transformer rules for all language constructs except loops, for which deriving a transformer rule remains an open problem. Finally, we show that the resulting weakest precondition variants have the same relations as in the classical case.

•Jan 1, 2026•0 citations

QbC: Quantum Correctness by Construction

Anurudh Peduri, Ina Schaefer, Michael Walter

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC) : an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

Proceedings of the ACM on Programming Languages•Apr 9, 2025•3 citations

Predicate Transformer Semantics of Quantum Programs

Mingsheng Ying, Runyao Duan, Yuan Feng +1 more

This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting. 8.1 Introduction In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques. Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.

Cambridge University Press eBooks•Nov 30, 2009•35 citations

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.

This article 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.

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

Nondeterminism has been introduced into quantum programming languages to model, for example, unspecified behavior. Weakest precondition transformers provide a formal framework for reasoning about program correctness with respect to a given postcondition. This thesis combines these ideas by introducing demonic and angelic interpretations of nondeterminism for quantum programs, together with corresponding weakest liberal precondition transformers. To capture angelic nondeterminism in a qualitative setting, we introduce predicates represented by sets of subspaces, where each subspace is represented by a projection. Such a predicate is satisfied whenever the quantum state belongs to one of the represented subspaces. We show, however, that natural definitions of the weakest liberal precondition transformer based on these predicates do not behave as desired for measurements and loops in the demonic setting. For this reason, the demonic weakest liberal precondition transformer is restricted to singleton postconditions. We further investigate the corresponding non-liberal weakest precondition transformers using termination spaces. This yields transformer rules for all language constructs except loops, for which deriving a transformer rule remains an open problem. Finally, we show that the resulting weakest precondition variants have the same relations as in the classical case.

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC) : an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting. 8.1 Introduction In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques. Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.