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 条
  • [1] FLOYD-HOARE LOGIC IN ITERATION THEORIES
    BLOOM, SL
    ESIK, Z
    [J]. JOURNAL OF THE ACM, 1991, 38 (04) : 887 - 934
  • [2] Inference Systems for Floyd-Hoare Logic with Partial Predicates
    Nikitchenko, Mykola
    Kryvolap, Andrii
    [J]. INFORMATICS 2013: PROCEEDINGS OF THE TWELFTH INTERNATIONAL CONFERENCE ON INFORMATICS, 2013, : 88 - 93
  • [3] Extended Floyd-Hoare Logic over Relational Nominative Data
    Nikitchenko, Mykola
    Ivanov, Ievgen
    Kornilowicz, Artur
    Kryvolap, Andrii
    [J]. INFORMATION AND COMMUNICATION TECHNOLOGIES IN EDUCATION, RESEARCH, AND INDUSTRIAL APPLICATIONS, ICTERI 2017, 2018, 826 : 41 - 64
  • [4] An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates
    Ivanov, Ievgen
    Kornilowicz, Artur
    Nikitchenko, Mykola
    [J]. FORMALIZED MATHEMATICS, 2018, 26 (02): : 159 - 164
  • [5] A General Framework for Sound and Complete Floyd-Hoare Logics
    Arthan, Rob
    Martin, Ursula
    Mathiesen, Erik A.
    Oliva, Paulo
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 11 (01)
  • [6] Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata
    Heizmann, Matthias
    Chen, Yu-Wen
    Dietsch, Daniel
    Greitschus, Marius
    Nutz, Alexander
    Musa, Betim
    Schaetzle, Claus
    Schilling, Christian
    Schuessele, Frank
    Podelski, Andreas
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II, 2017, 10206 : 394 - 398
  • [7] Deriving a Floyd-Hoare logic for non-local jumps from a formulae-as-types notion of control
    Crolard, T.
    Polonowski, E.
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2012, 81 (03): : 181 - 208
  • [8] Matching Logic: An Alternative to Hoare/Floyd Logic
    Rosu, Grigore
    Ellison, Chucky
    Schulte, Wolfram
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 2011, 6486 : 142 - +
  • [9] Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
    Feng, Yuan
    Li, Sanjiang
    [J]. INFORMATION AND COMPUTATION, 2023, 294
  • [10] THE HOARE LOGIC OF CONCURRENT PROGRAMS
    LAMPORT, L
    [J]. ACTA INFORMATICA, 1980, 14 (01) : 21 - 37
12345