A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic

• Main Authors: LE, Xuan Bach, LIN, Shang-Wei, SUN, Jun, SANAN, David
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2022
• Subjects: Quantum Computing; Verification; Formal Semantics; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/6919; https://ink.library.smu.edu.sg/context/sis_research/article/7922/viewcontent/3498697_pvoa_cc_by.pdf
• Institution: Singapore Management University

It is well-known that quantum programs are not only complicated to write but also tedious to verify due to their enormous state-space and the sophisticated mathematics beneath. In this work, we propose a Hoare-style inference framework to verify quantum programs. We infuse separation logic in our framework and invent the $\hoarule{qframe}$ rule, the quantum counterpart of the frame rule, to support local reasoning of quantum programs. The design of our framework is planned with a mindset for intuition and human-readability, using vectors in Dirac notation for reasoning instead of the orthodox matrix representation as in existing approaches. For evaluation, we apply our framework to verify various quantum programs such as Deutsch-Jozsa’s algorithm and Grover’s algorithm.