Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

TL;DR

This paper explores the relationships between abstract interpretation, Hoare logic, and incorrectness logic in the context of quantum programs, establishing how they induce each other and highlighting limitations in existing assertion frameworks.

Contribution

It demonstrates that complete quantum abstract interpretation induces sound and relatively complete quantum Hoare and incorrectness logics, and vice versa, with a focus on forward reasoning methods.

Findings

Induced logics are sound and relatively complete.

Forward reasoning makes the logics more applicable.

Certain assertion frameworks cannot support sound and complete logics.

Abstract

Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. All of them have been successfully extended to the quantum setting, but largely developed in parallel. In this paper, we examine the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. In particular, we show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both of which are sound and relatively complete. Unlike the logics proposed in the literature, the induced logic systems are in a forward manner, making them more useful in certain applications. Conversely, any sound and relatively complete quantum Hoare logic or quantum incorrectness logic induces a complete quantum abstract interpretation. As an application, we are able to show the non-existence of any sound and relatively complete quantum Hoare logic or incorrectness logic if tuples of local subspaces are taken as assertions.