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的语言，用于对特定流程构建的所有量子电路的输入输出状态编写断言。此外，它还提供了一种方法，可对测量结果的统计处理过程编写断言，以确保获得最终结果的流程正确性。这些断言可通过量子计算机模拟器自动验证。为评估效果，我们实现了该框架，并对一些广泛使用的量子算法编写了断言。实验结果表明，该框架具有足够的表达能力来验证量子软件的完整流程。