Practical Design by Contract Framework for Quantum Applications

Quantum application development typically involves verifying the construction procedures of quantum applications with a few qubits and running them on actual quantum computers based on the verified procedures. However, existing verification techniques face practical issues, such as the need for human intervention, long verification times, and insufficient descriptions. This study introduces a practical Design by Contract framework for quantum applications, designed for testing and debugging quantum applications on simulators. It allows for writing assertions about the input and output states of quantum circuits constructed by certain procedures and the post-processing of measurement results. The quantum application can be verified quickly by checking these assertions in test cases on simulators. Our framework introduces practical mechanisms for quantum application development. It separates the construction procedure of a quantum application and its assertions through parameter distinction, introduces an evaluation rule for early precondition checking, and reduces assertion-writing effort through assertion reuse mechanisms for inverting quantum circuits and using quantum circuits for qubits in a superposition state. We validated our framework through experiments and surveyed industry quantum computer researchers to assess its effectiveness.