A PROGRAMMING LOGIC FOR A VERIFIED STRUCTURED ASSEMBLY LANGUAGE

被引：0
|
作者：
CURZON, P
机构：
来源：
LECTURE NOTES IN ARTIFICIAL INTELLIGENCE | 1992年 / 624卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We describe a derived programming logic for a generic structured assembly language. It has been combined with a compiler correctness theorem. This allows us to deduce correctness properties of object code from corresponding properties of the source code proved with the programming logic. All proofs have been carried out using the HOL system.
引用
收藏
页码：403 / 408
页数：6
相关论文
共 50 条
  • [31] TEMPORAL LOGIC PROGRAMMING LANGUAGE TOKIO PROGRAMMING IN TOKIO
    AOYAGI, T
    FUJITA, M
    MOTOOKA, T
    LECTURE NOTES IN COMPUTER SCIENCE, 1986, 221 : 128 - 137
  • [32] THE PROGRAMMING LANGUAGE GCLA - A DEFINITIONAL APPROACH TO LOGIC PROGRAMMING
    ARONSSON, M
    ERIKSSON, LH
    GAREDAL, A
    HALLNAS, L
    OLIN, P
    NEW GENERATION COMPUTING, 1990, 7 (04) : 381 - 404
  • [33] Formal verification of a programming logic for a distributed programming language
    Zhang, C
    Olsson, RA
    Levitt, KN
    THEORETICAL COMPUTER SCIENCE, 1999, 216 (1-2) : 213 - 235
  • [34] A Formally Verified Interpreter for a Shell-Like Programming Language
    Jeannerod, Nicolas
    Marche, Claude
    Treinen, Ralf
    VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS (VSTTE 2017), 2017, 10712 : 1 - 18
  • [35] PROLOG - A LANGUAGE FOR PROGRAMMING MEDICAL LOGIC
    SHIFMAN, M
    JELOVSEK, FR
    M D COMPUTING, 1988, 5 (02): : 36 - &
  • [36] A language for programming logic with finite sets
    Dovier, Agostino
    Omodeo, Eugenio G.
    Pontelli, Enrico
    Rossi, Gianfranco
    Journal of Logic Programming, 1996, 28 (01):
  • [37] SEMANTICS OF PREDICATE LOGIC AS A PROGRAMMING LANGUAGE
    VANEMDEN, MH
    KOWALSKI, RA
    JOURNAL OF THE ACM, 1976, 23 (04) : 733 - 742
  • [38] Logic programming for processing natural language
    Dahl, V
    LOGIC PROGRAMMING - PROCEEDINGS OF THE 1997 INTERNATIONAL SYMPOSIUM, 1997, : 41 - 42
  • [39] LMNtal as a hierarchical logic programming language
    Ueda, Kazunori
    THEORETICAL COMPUTER SCIENCE, 2009, 410 (46) : 4784 - 4800
  • [40] A framed temporal logic programming language
    Duan, ZH
    Koutny, M
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2004, 19 (03) : 341 - 351
12345