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

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

4 转换的正确性证明

转换的形式化验证系统如图 5 所示, 系统的输入为编译前后的 Lustre 源程序和 C 目标程序, 输出为源程序和
目标程序语义一致性的证明序列, 以此说明编译系统编译的正确性. 在编译系统生成目标程序之后, 会给出 Lustre
源程序的文法单元序列以及目标程序的目标码模式序列; 同时可以获得源程序的操作语义以及目标程序的操作语
义. 随后通过操作语义构建出形式为前置条件的证明前提和形式为后置条件的证明目标. 最后, 在公理系统中根据
公理系统推导规则进行证明, 其中的证明序列主要针对源程序中每一条文法单元和对应目标码序列的语义一致
性, 而这部分可以分别手工证明每一条孤立的文法单元和对应目标码序列. 将手工的证明结果作为引理, 就可以自
动化地证明所需证明目标.

Lustre
Lustre 证明目标 公理系统 目标码
源代码 文法单元 转换模式
操作语义
Lustre 前置条件 公理系统
= 前置条件
C 前置条件 推导规则
Lustre 手工证明
前置后置
条件
目标码 证明序列 目标码
模式 序列推导
C 目标码
C 目标码 模式操作
语义
Lustre 后置条件
= 后置条件
C 前置 C 后置条件
后置条件

图 5 形式化验证系统架构图

证明目标的组成主要分为 3 个部分, 首先是假定 Lustre 源程序和 C 目标程序的输入相等, 即源程序中的输入
变量和目标程序中的输入变量一一对应相等. 在此基础上, 需要证明的目标就是源程序的输出变量和目标程序中
的输出变量一一对应相等, 而输出变量分别由源程序和目标程序根据输入变量计算得来.

4.1 文法单元和目标码模式的等价性证明
根据 Lustre 和 C 文法单元的操作语义的形式化表示, 构造证明序列证明单个的 Lustre 文法单元和对应 C 目
标码序列的操作语义的等价性. 以赋值语句<Equation>为例, 证明过程如下. 首先将证明目标分解为数个命题, 包
括 Lustre 和 C 的赋值语句定义命题, Lustre 和 C 的前置条件相等命题, Lustre 和 C 后置条件相等命题. 其中前 3
个命题为证明前提, 第 4 个命题为证明目标. 在本文形式化验证过程中所使用的符号集如附录 A 所示.
在表 7 中, 命题 P1、P2 和 P3 是证明的前提, P4 是证明的目标. 在表 8 中最后的推导结果 S8 : Lv6Id = left 即
需要证明的目标. 因此, Equation 文法在编译前后的语义具有一致性. 证明过程中, 公式 S1、S2 和 S3 分别由前提
得来, S4 由 S1、S2、和 S3 推导得来, 后续的公式 S5–S8 也类似.

表 7 赋值语句文法证明的命题

命题 说明
[ ]
P1 : (σ[expr] → σ[m]) ⇒ σ Equation → σ[Lv6Id/m]) Lustre赋值语句语义
[ ]
P2 : (σ c [expr c ] → σ c [m c ]) ⇒ σ c Equation c → σ c [left/m c ]) C赋值语句语义
[ ] [ ]
P3 : σ expr = σ c expr c 输入 (前置条件) 相等
P4 : Lv6Id = left 输出 (后置条件) 相等, 证明目标

图 6 是 Equation 文法在 Isabelle 中的证明代码序列, 主要分为 3 个部分: 对 Lustre 中 Equation 文法的形式
化定义, 对 Equation 文法的 C 目标码模式的形式化定义, 对上述两个定义的等价性证明. 由于 Isabelle 使用的是