Design by Contract Framework for Quantum Software
This addresses reliability issues for quantum software developers, though it is incremental as it builds on existing verification techniques.
The paper tackles the problem of ensuring correctness in quantum software beyond fixed circuits by proposing a design-by-contract framework that allows writing assertions for input/output states and measurement results, automatically checked via a simulator, and demonstrates sufficient expressive power for verifying entire quantum software procedures.
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.