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.

翻译：抽象解释、 Hoare 逻辑和不正确( 逆向 Hoare ) 逻辑是计算机程序静态分析的有力技术。 所有这些技术都成功地扩展到量子设置,但基本上平行发展。 在本文中,我们结合量子与程序核查这些技术之间的关系,抽象领域和量子国家的一套主张结构完善。特别是,我们表明,任何完整的量子抽象解释都引出量子Hare逻辑和量子不正确逻辑,两者都是合理和相对完整的。与文献中提议的逻辑不同,引导逻辑系统是前瞻性的,在某些应用中更有用。相反,任何合理和相对完整的量子体逻辑或量子不正确逻辑都引出完整的量子抽象解释。作为一个应用,如果将本地子空间的图象视为断言,我们就能显示不存在任何声音和相对完整的量子Hare逻辑或不正确逻辑。