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

于涛 等: 基于下推自动机的同步数据流语言可信编译 3563

函数式语言, 其形式化表示与上文表格中的语义定义在形式上有所不同. equation_lustre 以函数式的形式定义
了 Lustre 中赋值语句的语义, 该函数接受两个表达式, 并返回第 2 个表达式的值. Equation_c 也同理. lemma
equivalence_prioerty_equation 是一个引理, 一个引理需要被证明, 也可以在被证明后用于其他引理的证明. 在本文
中表示为证明目标: 先前定义的两个函数是等价的, 具体是指, 假设两个函数的输入是相等的, 那么他们的返回值
也相等.

表 8 赋值文法证明过程

公式 证据
[ ] [ ]
S1 : σ expr = σ c expr c P3
[ ]
S2 : σ expr → σ[m] P1
[ ]
S3 : σ c expr c → σ[m c ] P2
S4 : m = m c S1,S2,S3
[ ]
S5 : σ Equation → σ[Lv6Id/m]) P1
[ ]
S6 : σ c Equation c → σ c [left/m c ]) P2
[ ]
S7 : σ c Equation c → σ c [left/m]) S4,S6
S8 : Lv6Id = left S5,S7

图 6 Equation 文法 Isabelle 证明序列

图 7 为 Isabelle 中开始证明前, 分别运行两条证明语句之后的证明目标. 第 1 个部分尚未开始证明, 证明目标
即 lemma 中的证明目标 (shows 之后的部分). 第 2 部分为运行了第 1 条证明语句 unfolding equation_lustre_
defequation_c_def 后的结果, 该语句展开了上文对 equation_lustre 和 Equation_c 的定义并自动化简, 由此证明目标
∀t.expression2_lt = expression2_ct, 而这正好和证明的前提相同. 因此第 2 条语句 using preconditions by
变为了
auto 表示自动应用证明前提, 这就完成了对该引理的证明, 也即 Equation 的文法单元和目标码序列是等价的. 通
过这种方式, 可以独立地证明每条文法和对应目标码模式的语义等价性.

图 7 证明过程中的证明目标变化

4.2 源程序和目标程序等价性证明
通过下推自动机识别能得到编译前后的源程序和目标程序的文法单元, 从而生成对应的程序整体的语义, 即