Provably Correct Code Generation: A Case Study

被引：2
|
作者：
Wang, Qian [1 ]
Gupta, Gopal [1 ]
机构：
[1] Univ Texas Dallas, Dept Comp Sci, Dallas, TX 75083 USA
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 118卷
关键词：
Horn logic; Denotational Semantics; Compilation;
D O I：
10.1016/j.entcs.2004.11.008
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we present an approach to provably correct compilation based on Horn logical semantics of programming languages and partial evaluation. We also show that continuation semantics can be expressed in the Horn logical framework, and introduce Definite Clause Semantics. We illustrate our approach by developing the semantics for the SCR specification language, and using it to (automatically) generate target code in a provably correct manner.
引用
收藏
页码：87 / 109
页数：23
相关论文
共 50 条
  • [31] Provably Correct Safety Protocol for Cooperative Platooning
    Mair, Sebastian
    Althoff, Matthias
    2024 35TH IEEE INTELLIGENT VEHICLES SYMPOSIUM, IEEE IV 2024, 2024, : 780 - 787
  • [32] Provably Correct Controller Synthesis of Switched Stochastic Systems with Metric Temporal Logic Specifications: A Case Study on Power Systems
    Xu, Zhe
    Zhang, Yichen
    2021 60TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2021, : 3519 - 3524
  • [33] CASE-STUDY OF A NEW CODE GENERATION TECHNIQUE FOR COMPILERS
    CARTER, JL
    COMMUNICATIONS OF THE ACM, 1977, 20 (12) : 914 - 920
  • [34] Code generation by model transformation: a case study in transformation modularity
    Zef Hemel
    Lennart C. L. Kats
    Danny M. Groenewegen
    Eelco Visser
    Software & Systems Modeling, 2010, 9 : 375 - 402
  • [35] Model driven development and code generation: An automotive case study
    Banci, Michele
    Fantechi, Alessandro
    Gnesi, Stefania
    Lombardi, Giovanni
    SDL 2007: DESIGN FOR DEPENDABLE SYSTEMS, PROCEEDINGS, 2007, 4745 : 19 - 34
  • [36] Code generation by model transformation: a case study in transformation modularity
    Hemel, Zef
    Kats, Lennart C. L.
    Groenewegen, Danny M.
    Visser, Eelco
    SOFTWARE AND SYSTEMS MODELING, 2010, 9 (03): : 375 - 402
  • [37] Code generation by model transformation - A case study in transformation modularity
    Hemel, Zef
    Kats, Lennart C. L.
    Visser, Eelco
    THEORY AND PRACTICE OF MODEL TRANSFORMATIONS, 2008, 5063 : 183 - 198
  • [38] Correct-by-construction code generation from hybrid automata specification
    Bresolin, Davide
    Di Guglielmo, Luigi
    Geretti, Luca
    Villa, Tiziano
    2011 7TH INTERNATIONAL WIRELESS COMMUNICATIONS AND MOBILE COMPUTING CONFERENCE (IWCMC), 2011, : 1660 - 1665
  • [39] Provably correct reactive control from natural language
    Lignos, Constantine
    Raman, Vasumathi
    Finucane, Cameron
    Marcus, Mitchell
    Kress-Gazit, Hadas
    AUTONOMOUS ROBOTS, 2015, 38 (01) : 89 - 105
  • [40] Provably correct reactive control from natural language
    Constantine Lignos
    Vasumathi Raman
    Cameron Finucane
    Mitchell Marcus
    Hadas Kress-Gazit
    Autonomous Robots, 2015, 38 : 89 - 105
12345