A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic

Abstract

Quantum programs are not only complicated to design but also challenging to verify, as quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To address the state-space explosion problem in quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we integrate separation logic into our framework and enable local reasoning via a quantum frame rule analogous to the classical frame rule. For evaluation, we apply our framework to verify representative quantum programs, including Deutsch–Jozsa's algorithm and Grover's algorithm.