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 complete program and only then verifies its correctness. In this work, 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 a set of refinement rules to construct correct programs in a quantum while language. We validate QbC by constructing quantum programs for two idiomatic problems, teleportation and search, from their specification. 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 an important role in supporting the design and taxonomization of quantum algorithms and software.

翻译：摘要：得益于量子算法的快速进展与日益复杂性，量子程序的正确性已成为一个主要关注点。过去数年的开创性研究提出了多种方法，通过诸如量子霍尔逻辑等证明系统对量子程序进行形式化验证。所有这些先前方法都是事后验证的：先实现完整程序，再验证其正确性。本研究提出“按构造保证量子正确性”（QbC）：一种从规范出发构造量子程序以确保正确性的方法。我们使用前置条件和后置条件来指定程序属性，并提出一组精化规则，用于在量子while语言中构造正确程序。我们通过从规范出发构造两个典型问题（量子隐形传态与搜索）的量子程序对QbC进行了验证。研究发现，该方法能自然揭示程序细节的推导过程，并突出沿途的关键设计选择。因此，我们相信QbC能在支持量子算法与软件的设计及分类中发挥重要作用。