Weakest preconditions for high-level programs

被引：0
|
作者：
Habel, Annegret [1 ]
Pennemann, Karl-Heinz
Rensink, Arend
机构：
[1] Carl von Ossietzky Univ Oldenburg, D-2900 Oldenburg, Germany
[2] Univ Twente, NL-7500 AE Enschede, Netherlands
来源：
GRAPH TRANSFORMATIONS, PROCEEDINGS | 2006年 / 4178卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented.
引用
收藏
页码：445 / 460
页数：16
相关论文
共 50 条
  • [1] Weakest preconditions for pure Prolog programs
    Pedreschi, D
    Ruggieri, S
    [J]. INFORMATION PROCESSING LETTERS, 1998, 67 (03) : 145 - 150
  • [2] Efficient weakest preconditions
    Rustan, K
    Leino, M
    [J]. INFORMATION PROCESSING LETTERS, 2005, 93 (06) : 281 - 288
  • [3] Weakest preconditions in fibrations
    Aguirre, Alejandro
    Katsumata, Shin-ya
    Kura, Satoshi
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2022, 32 (04) : 472 - 510
  • [4] Quantum weakest preconditions
    D'Hondt, Ellie
    Panangaden, Prakash
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (03) : 429 - 451
  • [5] CHARACTERIZATION OF WEAKEST PRECONDITIONS
    WAND, M
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1977, 15 (02) : 209 - 212
  • [6] Weakest Preconditions in Fibrations
    Aguirre, Alejandro
    Katsumata, Shin-ya
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2020, 352 (352) : 5 - 27
  • [7] Software Reliability Analysis Using Weakest Preconditions in Linear Assignment Programs
    Luo, Hang
    Liu, Xue
    Chen, Xi
    Long, Ting
    Jiang, Ronghua
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2016, 42 (09) : 866 - 885
  • [8] High-Level Programs and Program Conditions
    Azab, Karl
    Habel, Annegret
    [J]. GRAPH TRANSFORMATIONS, ICGT 2008, 2008, 5214 : 211 - 225
  • [9] HIGH-LEVEL CONTROL PROGRAMS AT NSLS
    BOZOKI, ES
    [J]. LECTURE NOTES IN PHYSICS, 1984, 215 : 420 - 424
  • [10] Generalised quantum weakest preconditions
    Roman Gielerak
    Marek Sawerwain
    [J]. Quantum Information Processing, 2010, 9 : 441 - 449
12345