To realize reliable quantum software, techniques to automatically ensure the quantum software's correctness have recently been investigated. However, they primarily focus on fixed quantum circuits rather than the procedure of building quantum circuits. Despite being a common approach, the correctness of building circuits using different parameters following the same procedure is not guaranteed. To this end, we propose a design-by-contract framework for quantum software. Our framework provides a python-embedded language to write assertions on the input and output states of all quantum circuits built by certain procedures. Additionally, it provides a method to write assertions about the statistical processing of measurement results to ensure the procedure's correctness for obtaining the final result. These assertions are automatically checked using a quantum computer simulator. For evaluation, we implemented our framework and wrote assertions for some widely used quantum algorithms. Consequently, we found that our framework has sufficient expressive power to verify the whole procedure of quantum software.
翻译:为了实现可靠的量子软件,最近已经研究了自动确保量子软件正确性的技术。然而,它们主要关注的是固定的量子电路,而不是构建量子电路的过程。尽管这是一种常见的方法,但是使用不同的参数按照相同的程序构建电路的正确性不能保证。为此,我们提出了一种设计合约框架,用于量子软件。我们的框架提供了一个嵌入式的Python语言来编写关于某些程序构建的所有量子电路的输入和输出状态的断言。此外,它提供了一种方法来编写关于测量结果的统计处理的断言,以确保获得最终结果的过程的正确性。这些断言使用量子计算机模拟器自动检查。为了评估,我们实现了我们的框架并编写了一些广泛使用的量子算法的断言。因此,我们发现我们的框架具有足够的表达能力来验证整个量子软件的过程。