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

被引:8
作者
Feng, Yuan [1 ]
Li, Sanjiang [1 ]
机构
[1] Univ Technol Sydney, Ctr Quantum Software & Informat, Ultimo, Australia
基金
澳大利亚研究理事会;
关键词
Quantum programming; Abstract interpretation; Incorrectness logic;
D O I
10.1016/j.ic.2023.105077
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. They have all been successfully extended to the quantum setting, but developed largely in parallel. This paper explores the relationship between these techniques in the context of verifying quantum whileprograms, where the abstract domain and the set of assertions for quantum states are wellstructured. We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both being sound and relatively complete. Moreover, the induced logic systems operate in a forward manner, making them more suitable for certain applications. Conversely, any sound and relatively complete quantum Hoare logic or incorrectness logic induces a complete quantum abstract interpretation. As an application, we 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. & COPY; 2023 Elsevier Inc. All rights reserved.
引用
收藏
页数:22
相关论文
共 35 条
[31]  
Ying M., 2014, arXiv
[32]   A proof system for disjoint parallel quantum programs [J].
Ying, Mingsheng ;
Zhou, Li ;
Li, Yangjia ;
Feng, Yuan .
THEORETICAL COMPUTER SCIENCE, 2022, 897 :164-184
[33]   Floyd-Hoare Logic for Quantum Programs [J].
Ying, Mingsheng .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2011, 33 (06)
[34]   Quantum Abstract Interpretation [J].
Yu, Nengkun ;
Palsberg, Jens .
PROCEEDINGS OF THE 42ND ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '21), 2021, :542-558
[35]   An Applied Quantum Hoare Logic [J].
Zhou, Li ;
Yu, Nengkun ;
Ying, Mingsheng .
PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, :1149-1162