将C11代码支持深度集成于Isabelle / PIDE

• 2019 年 12 月 29 日
• 笔记

原文题目: Deeply Integrating C11 Code Support into Isabelle/PIDE

摘要： 我们提出了一个C11语法的C代码框架，并将其深入集成到Isabelle/PIDE开发环境中。我们的框架为独立插入的验证后端提供了一个抽象接口。因此，可以将各种技术（如演绎程序验证或白盒测试）应用于同一个源，该源是集成PIDE文档模型的一部分。语义后端可以自由选择支持的C片段及其语义，亮点在于它们可以在所选择的内存模型或帧条件的规范机制上有所不同。

我们的框架以注释的形式支持C源的语义注释。注释用于本地控制后端设置，并可以表示注释所指的术语焦点。在计算语义注释时，逻辑上下文和语法上下文都是可用的。因此，注释中的公式可以引用HOL或C变量。

我们的方法证明了Isabelle/PIDE子系统近年来所达到的成熟度和表达能力。我们的集成技术使用Lex和Yacc风格的语法来确保高效的确定性解析。为了验证后端接口的设计决策，我们提出了两个集成（已知）语义后端的案例研究。

原文作者：Frédéric Tuong (LRI, Université Paris-Saclay), Burkhart Wolff (LRI, Université Paris-Saclay)

原文地址：https://arxiv.org/abs/1912.10630