Reverse Hoare Logic

被引：0
|
作者：
de Vries, Edsko [1 ]
Kontavas, Vasileios [1 ]
机构：
[1] Trinity Coll Dublin, Dublin, Ireland
来源：
SOFTWARE ENGINEERING AND FORMAL METHODS | 2011年 / 7041卷
关键词：
PROGRAM INVERSION; REFINEMENT;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a novel Hoare-style logic, called Reverse Hoare Logic, which can be used to reason about state reachability of imperative programs. This enables us to give natural specifications to randomized (deterministic or nondeterministic) algorithms. We give a proof system for the logic and use this to give simple formal proofs for a number of illustrative examples. We define a weakest postcondition calculus and use this to show that the proof system is sound and complete.
引用
收藏
页码：155 / 171
页数：17
相关论文
共 50 条
  • [1] Hoare logic in the abstract
    Martin, Ursula
    Mathiesen, Erik A.
    Oliva, Paulo
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 501 - 515
  • [2] 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
  • [3] HOARE LOGIC, EXECUTABLE SPECIFICATIONS, AND LOGIC PROGRAMS
    FUCHS, NE
    [J]. STRUCTURED PROGRAMMING, 1992, 13 (03): : 129 - 135
  • [4] Matching Logic: An Alternative to Hoare/Floyd Logic
    Rosu, Grigore
    Ellison, Chucky
    Schulte, Wolfram
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 2011, 6486 : 142 - +
  • [5] An Applied Quantum Hoare Logic
    Zhou, Li
    Yu, Nengkun
    Ying, Mingsheng
    [J]. PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 1149 - 1162
  • [6] EXPRESSIVENESS AND THE COMPLETENESS OF HOARE LOGIC
    BERGSTRA, JA
    TUCKER, JV
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (03) : 267 - 284
  • [7] A DECOMPOSITION RULE FOR THE HOARE LOGIC
    TAKAOKA, T
    [J]. INFORMATION PROCESSING LETTERS, 1987, 26 (04) : 205 - 208
  • [8] On the completeness of propositional Hoare logic
    Kozen, D
    Tiuryn, J
    [J]. INFORMATION SCIENCES, 2001, 139 (3-4) : 187 - 195
  • [9] HOARE LOGIC AND PEANO ARITHMETIC
    BERGSTRA, JA
    TUCKER, JV
    [J]. THEORETICAL COMPUTER SCIENCE, 1983, 22 (03) : 265 - 284
  • [10] THE HOARE LOGIC OF CONCURRENT PROGRAMS
    LAMPORT, L
    [J]. ACTA INFORMATICA, 1980, 14 (01) : 21 - 37
12345