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

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

给出证明, 如图 9 是对 merge 运算符的语义一致性证明, 本节共对表达式文法单元中的 15 种运算符给出了语义一
致性证明.

表 9 表达式文法测试用例个数统计

表达式文法单元 测试用例个数
<constant> 3
布尔运算符 2
算数运算符 3
比较运算符 3
int <Expression> 2
real <Expression> 2
pre <Expression> 3
current <Expression> 4
<Expression> fby <Expression> 3
<Expression> → <Expression> 3
if <Expression> then <Expression> else <Expression> 3
# (<Expression>) 2
nor (<Expression>) 2
merge <Lv6Id> <Mergecaselist> 4
<CallByPosExpression> 3
<CallByNameExpression> 4
[<ExpressionList>] 2
<Expression> ^ <Expression> 2
<Expression> | <Expression> 2
<Expression>[<Expression>] 2
<Expression> . <Lv6Id> 2
(<ExpressionList>) 2
运算符组合测试 20
总计 78

图 9 merge 运算符一致性证明

根据单个运算符文法的语义一致性证明, 可以由此进行程序的一致性证明. 本节对包含了上述 15 种文法的
10 个 Lustre 程序进行了验证测试, 平均证明长度 (含定义) 为 15 行. 由 Isabelle 对语义一致性证明序列进行自动推
理并得到程序语义一致证明结论, 从而说明该形式化验证方法的有效性.

5.3 系统运行耗时结果分析
表 10 给出编译系统各个阶段的平均运行时间和生成的目标代码运行 1 000 万周期的时间, 其中下推自动机
生成仅需执行一次, 在每次编译时不需要执行. 在系统建模的实际生产中, 通常不会频繁进行编译, 因此对于编译
的时间效率并不敏感.