Page 141 - 《软件学报》2025年第8期

3564 软件学报 2025 年第 36 卷第 8 期

在 Isabelle/HOL 中以 Iris 语言建模的形式化表示. 程序整体的语义由各个语法单元的语义组成, 而每条语法单元
的语义的等价性在第 4.1 节当中得到了证明. 因此, 可以利用语法单元语义一致的结论证明程序的语义一致性.
图 8 展示了一个包含了加法和 pre 运算符的 Lustre 程序和对应 C 程序一致性的证明序列. 与第 4.1 节中的证明
过程类似, definition usepre_lustre 和 definition usepre_c 分别是 Lustre 语言和 C 语言代码的定义, 其中 add_lustre、
add_c、pre_lustre、pre_c 已经分别定义且证明了等价性. 所以, 在等价性引理 lemma equivalence_property_usepre
的证明中, 只需要分别对它们进行展开并进行化简, 就可以证明它们之间的一致性.

图 8 程序语义一致性证明序列

上文的证明体现出, 在已经定义了子文法的语义和证明了子文法语义的一致性的基础上, 对于程序一致性的
证明在 Isabelle 中可以通过如下的方法证明.
(1) 定义 Lustre 源程序和 C 目标程序的语义, Lustre 程序和 C 程序的语义由其子文法递归给出;
(2) 定义证明前提和证明目标, 其中证明前提为 Lustre 和 C 程序的前置条件相等, 证明目标为 Lustre 和 C 程
序的后置条件相等;
(3) 将 (1) 中定义的 Lustre 和 C 程序语义使用 unfolding 命令以文法单元为单位依次展开并化简;
(4) 使用 using preconditions by auto 命令应用证明前提 (即前置条件相等) 并进行自动推理并得到证明结论.
Isabelle 的自动推理能力有限, 但经过 (3) 的展开, 其形式已经可以自动推导出结论.

5 实验与分析

本节展示了对提出的基于下推自动机的 Lustre 语言可信编译器进行系统测试的过程和结果, 测试在指定的实
验环境 (处理器为 Intel Core i5-13600KF CPU @ 3.50 GHz, 内存为 32 GB, 操作系统为 Windows 11) 下进行.

5.1 代码生成测试结果与分析
代码生成测试主要进行功能测试, 即测试代码生成的结果是否正确, 测试需要对编译器实现的所有 Lustre 文
法进行测试. Lustre V6 版本共有 73 个文法单元, 本文实现的编译器共支持其中的 72 个. 在 72 个文法单元中, 程
序结构定义文法有 49 条, 核心的赋值语句和表达式文法有 23 条. 其中程序结构定义文法在每次测试中都会涉及,
只需单独测试其中不常用的部分, 赋值语句和表达式文法为测试的重点.
针对 72 个文法单元和对应的 218 个产生式, 本文共构建了 150 个以上的基本测试用例, 旨在测试单条文法的
正确性. Lustre 中核心的表达式文法的测试用例数如后文表 9 所示, 其中运算符组合测试是在一个表达式中使用
多个运算符, 测试运算符之间的优先级结合性等关系是否正确.
对生成的 C 代码进行静态分析, 检查是否存在语法错误, 并将本文编译器生成的代码和官方代码生成器生成
的代码的运行结果进行比较, 观察运行结果是否符合预期. 经过测试, 本文实现的代码生成模块在涉及的所有文法
单元中均能正确生成目标代码.

5.2 形式化验证测试结果与分析
形式化验证测试需要针对 Lustre 文法单元给出对应的语义一致性证明. 首先需要对单个运算符的语义一致性