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 条
  • [31] VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
    Qinxiang Cao
    Lennart Beringer
    Samuel Gruetter
    Josiah Dodds
    Andrew W. Appel
    [J]. Journal of Automated Reasoning, 2018, 61 : 367 - 422
  • [32] THE HOARE LOGIC OF CSP, AND ALL THAT
    LAMPORT, L
    SCHNEIDER, FB
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1984, 6 (02): : 281 - 296
  • [33] VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
    [J]. Appel, Andrew W. (appel@princeton.edu), 1600, Springer Science and Business Media B.V. (61): : 1 - 4
  • [34] VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
    Cao, Qinxiang
    Beringer, Lennart
    Gruetter, Samuel
    Dodds, Josiah
    Appel, Andrew W.
    [J]. JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) : 367 - 422
  • [35] EXPRESSIVENESS AND THE COMPLETENESS OF HOARE LOGIC
    BERGSTRA, JA
    TUCKER, JV
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (03) : 267 - 284
  • [36] Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
    Nagy, Shaan
    Kim, Jinwoo
    Reps, Thomas
    D'Antoni, Loris
    [J]. Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA2) : 113 - 139
  • [37] A DECOMPOSITION RULE FOR THE HOARE LOGIC
    TAKAOKA, T
    [J]. INFORMATION PROCESSING LETTERS, 1987, 26 (04) : 205 - 208
  • [38] On the completeness of propositional Hoare logic
    Kozen, D
    Tiuryn, J
    [J]. INFORMATION SCIENCES, 2001, 139 (3-4) : 187 - 195
  • [39] HOARE LOGIC AND PEANO ARITHMETIC
    BERGSTRA, JA
    TUCKER, JV
    [J]. THEORETICAL COMPUTER SCIENCE, 1983, 22 (03) : 265 - 284
  • [40] A Hoare logic for linear systems
    Arthan, Rob
    Martin, Ursula
    Oliva, Paulo
    [J]. FORMAL ASPECTS OF COMPUTING, 2013, 25 (03) : 345 - 363
12345