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 条
  • [41] HOARE LOGIC OF DISTRIBUTED REDUNDANT-SYSTEMS
    MANCINI, L
    PAPPALARDO, G
    [J]. COMPUTING SYSTEMS, 1988, 3 (04): : 171 - 180
  • [42] Hoare logic for realistically modelled machine code
    Myreen, Magnus O.
    Gordon, Michael J. C.
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 568 - +
  • [43] Hoare logic-based genetic programming
    He Pei
    Kang LiShan
    Johnson, Colin G.
    Ying Shi
    [J]. SCIENCE CHINA-INFORMATION SCIENCES, 2011, 54 (03) : 623 - 637
  • [44] Monad-independent Hoare logic in HASCASL
    Schröder, L
    Mossakowski, T
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2621 : 261 - 277
  • [45] PROVING PROGRAM INCLUSION USING HOARE LOGIC
    BERGSTRA, JA
    KLOP, JW
    [J]. THEORETICAL COMPUTER SCIENCE, 1984, 30 (01) : 1 - 48
  • [46] THE USE OF HOARE LOGIC IN THE VERIFICATION OF HORIZONTAL MICROPROGRAMS
    DASGUPTA, S
    WAGNER, A
    [J]. INTERNATIONAL JOURNAL OF COMPUTER & INFORMATION SCIENCES, 1984, 13 (06): : 461 - 490
  • [47] A Hoare Logic for the State Monad Proof Pearl
    Swierstra, Wouter
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2009, 5674 : 440 - 451
  • [48] Floyd-Hoare Logic for Quantum Programs
    Ying, Mingsheng
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2011, 33 (06):
  • [49] Using Hoare Logic in a Process Algebra Setting
    Bergstra, J. A.
    Middelburg, C. A.
    [J]. FUNDAMENTA INFORMATICAE, 2021, 179 (04) : 321 - 344
  • [50] FLOYD-HOARE LOGIC IN ITERATION THEORIES
    BLOOM, SL
    ESIK, Z
    [J]. JOURNAL OF THE ACM, 1991, 38 (04) : 887 - 934
12345