External Behavior of a Logic Program and Verification of Refactoring

被引：2
|
作者：
Fandinno, Jorge [1 ]
Hansen, Zachary [1 ]
Lierler, Yuliya [1 ]
Lifschitz, Vladimir [2 ]
Temple, Nathan [2 ]
机构：
[1] Univ Nebraska, Omaha, NE 68182 USA
[2] Univ Texas Austin, Austin, TX USA
来源：
THEORY AND PRACTICE OF LOGIC PROGRAMMING | 2023年 / 23卷 / 04期
关键词：
answer set programming; software verification; proof assistant; automated reasoning;
D O I：
10.1017/S1471068423000200
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.
引用
收藏
页码：933 / 947
页数：15
相关论文
共 50 条
  • [1] Program Verification with Separation Logic
    Iosif, Radu
    MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 48 - 62
  • [2] A DYNAMIC LOGIC FOR PROGRAM VERIFICATION
    HEISEL, M
    REIF, W
    STEPHAN, W
    LECTURE NOTES IN COMPUTER SCIENCE, 1989, 363 : 134 - 145
  • [3] A program logic for resource verification
    Aspinall, D
    Beringer, L
    Hofmann, M
    Loidl, HW
    Momigliano, A
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2004, 3223 : 34 - 49
  • [4] Refactoring logic programs
    Serebrenik, A
    Demoen, B
    LOGIC PROGRAMMING, PROCEEDINGS, 2003, 2916 : 509 - 510
  • [5] Logic plus control: On program construction and verification
    Drabent, Wlodzimierz
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2018, 18 (01) : 1 - 29
  • [6] A Program Construction and Verification Tool for Separation Logic
    Dongol, Brijesh
    Gomes, Victor B. F.
    Struth, Georg
    MATHEMATICS OF PROGRAM CONSTRUCTION, MPC 2015, 2015, 9129 : 137 - 158
  • [7] Completeness of Pointer Program Verification by Separation Logic
    Tatsuta, Makoto
    Chin, Wei-Ngan
    Al Ameen, Mahmudul Faisal
    SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2009, : 179 - +
  • [8] Towards mechanized program verification with separation logic
    Weber, T
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 250 - 264
  • [9] Exploiting Refactoring in Formal Verification
    Yin, Xiang
    Knight, John
    Weimer, Westley
    2009 IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS & NETWORKS (DSN 2009), 2009, : 53 - 62
  • [10] Verification and refactoring of ontologies with rules
    Baumeister, Joachim
    Seipel, Dietmar
    MANAGING KNOWLEDGE IN A WORLD OF NETWORKS, PROCEEDINGS, 2006, 4248 : 82 - 95
12345