Floyd-Hoare Logic for Quantum Programs

被引：69
|
作者：
Ying, Mingsheng [1 ,2 ]
机构：
[1] Univ Technol Sydney, Ctr Quantum Computat & Intelligent Syst, Fac Engn & Informat Technol, City Campus,15 Broadway, Ultimo, NSW 2007, Australia
[2] Tsinghua Univ, State Key Lab Intelligent Technol & Syst, Tsinghua Natl Lab Informat Sci & Technol, Dept Comp Sci & Technol, Beijing 100084, Peoples R China
来源：
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2011年 / 33卷 / 06期
基金：
中国国家自然科学基金; 澳大利亚研究理事会;
关键词：
Theory; Languages; Quantum computation; programming language; axiomatic semantics; Floyd-Hoare logic; completeness;
D O I：
10.1145/2049706.2049708
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Floyd-Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd-Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
引用
收藏
页数：49
相关论文
共 50 条
  • [21] Verifying BPEL-like programs with Hoare logic
    Luo C.
    Qin S.
    Qiu Z.
    [J]. Front. Comput. Sci. China, 2008, 4 (344-356): : 344 - 356
  • [22] HOARE LOGIC FOR NONDETERMINISTIC REGULAR PROGRAMS - A NONSTANDARD APPROACH
    HORTALAGONZALEZ, MT
    RODRIGUEZARTALEJO, M
    [J]. THEORETICAL COMPUTER SCIENCE, 1989, 68 (03) : 277 - 302
  • [23] Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
    Liu, Junyi
    Zhan, Bohua
    Wang, Shuling
    Ying, Shenggang
    Liu, Tao
    Li, Yangjia
    Ying, Mingsheng
    Zhan, Naijun
    [J]. COMPUTER AIDED VERIFICATION, CAV 2019, PT II, 2019, 11562 : 187 - 207
  • [24] HOARE LOGIC FOR PROGRAMS WITH PROCEDURES - WHAT HAS BEEN ACHIEVED
    OLDEROG, ER
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1984, 164 : 383 - 395
  • [25] HOARE LOGIC FOR NONDETERMINISTIC REGULAR PROGRAMS - A NONSTANDARD COMPLETENESS THEOREM
    HORTALAGONZALEZ, T
    RODRIGUEZARTALEJO, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 194 : 270 - 280
  • [26] Reverse Hoare Logic
    de Vries, Edsko
    Kontavas, Vasileios
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 155 - 171
  • [27] Hoare logic in the abstract
    Martin, Ursula
    Mathiesen, Erik A.
    Oliva, Paulo
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 501 - 515
  • [28] Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs
    Kawamoto, Yusuke
    Sato, Tetsuya
    Suenaga, Kohei
    [J]. ARTIFICIAL INTELLIGENCE, 2024, 326
  • [29] Dynamic quantum logic for quantum programs
    Brunet, O
    Jorrand, P
    [J]. INTERNATIONAL JOURNAL OF QUANTUM INFORMATION, 2004, 2 (01) : 45 - 54
  • [30] On Incorrectness Logic for Quantum Programs
    Yan, Peng
    Jiang, Hanru
    Yu, Nengkun
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (OOPSLA):
12345