一句话：提出 QbC 方法，用前后置条件与可靠完备的精化规则从规约构造正确的量子程序。
量子算法快速发展且日益复杂，量子程序正确性成为重要问题。已有工作多采用量子 Hoare 逻辑等证明系统进行事后验证，即先实现程序再验证。本文提出 Quantum Correctness by Construction（QbC），从规约出发构造量子程序并同时保证正确性。方法使用前置条件和后置条件描述程序性质，并为量子 while 语言提出可靠且完备的精化规则，支持从规约逐步构造程序。作者通过为若干惯用量子问题与模式构造程序来验证 QbC，发现该方法能自然引导推导程序细节并凸显关键设计选择，有望支持量子算法与软件的设计和分类。
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.
@article{paperbot3213,
title = {QbC: Quantum Correctness by Construction},
author = {Anurudh Peduri and Ina Schaefer and Michael Walter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720433}
}