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

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

表 A1 符号集

类型 符号 意义
σ 程序取值集合, 表示当前的程序运行状态, 每个周期都会有这样一个取值集合
σ[c] 表示在状态 σ 下执行程序c
σ −i 表示在 i 周期前的程序状态
n
n
σ [c] 表示在状态 σ 下执行程序 c, 每个周期都有一个状态集合
语义符号 σ[x/v] 定义一个新状态, 程序变量 x 在该状态下的值为 v
σ[( x : t)/v] 定义一个新状态, 程序变量 x 在该状态下的值为 v, 类型为 t
σ[c] → σ 1 程序在状态 σ 下运行 c 后到达终止状态 σ 1
σ → cur 表示将 σ 设为当前周期;
σ[c] → σ 1 [c1] 程序在状态 σ 下运行 c 后得到的结果为状态 σ 1 , 且下一步要执行的程序为 c1
¬ 一元联结词, 非
逻辑 → 二元联结词, 蕴含
联结词 ∨ 二元联结词, 或
二元联结词, 且
∧
= 一元运算符, 赋值
运算符 < 二元运算符, 小于
> 二元运算符, 大于

附录 B. Lustre 操作语义

由于篇幅限制, 以下给出 Lustre 部分文法的操作语义表示. 表 B1 是 Lustre 表达式单元文法 (时态和时钟运算
符部分) 的操作语义. 时态运算符 pre 用于获取表达式在上个周期的值, 假设表达式 expr1 在上个周期的语境 σ −1
中的取值为 m, 则该表达式 (pre expr1) 在当前语境 σ 下的取值为 m. 时钟运算符 when 用于指定流的时钟周期, 若
时钟表达式 ClockExpr 在当前语境 σ 的取值为 true, expr1 在 σ 的取值为 m, 则表达式 expr 在 σ 的取值为 m; 若时
钟表达式 ClockExpr 在当前语境 σ 的取值为 false, 则表达式 expr 在 σ 的取值为 nil. current 运算符用于将非基础
周期的流转化为基础周期的流, 若表达式 expr1 的时钟在当前语境 σ 的取值为 true 且 expr1 在 σ 的取值为 m, 则
expr 在 σ 的取值为 m, 若表达式 expr1 的时钟在当前周期内取值为 false 且 expr 在上个周期的语境 σ −1 的取值为
m, 则 expr 在 σ 的取值为 m.

表 B1 Lustre 表达式文法单元语义定义 (时态和时钟运算符部分)

结构元素 文法单元 前置/后置条件
( [ ] ) ( [ ] )
pre < expr1 > σ −1 expr1 → σ −1 [m] ⇒ σ expr → σ[m]
( [ ] ) ( [ ] )
第1周期, σ expr1 → σ[m] ⇒ σ expr → σ[m]
< expr1 > arrow < expr2 >
( [ ] ) ( [ ] )
非第1周期, σ expr2 → σ[m] ⇒ σ expr → σ[m]
( [ ] ) ( [ ] )
第1周期, σ expr1 → σ[m] ⇒ σ expr → σ[m]
< expr1 > fby < expr2 >
< expr > ( −1 [ ] −1 ) ( [ ] )
非第1周期, σ expr2 → σ [m] ⇒ σ expr → σ[m]
( [ ] [ ] ) ( [ ] )
σ ClockExpr → σ[true],σ expr1 → σ[m] ⇒ σ expr → σ[m]
< expr1 > when < ClockExpr > ( [ ] ) ( [ ] )
σ ClockExpr → σ[false] ⇒ σ expr → σ[nil]
( [ ] ) ( [ ] −1 [ ] )
σ expr1.Clock → σ[false] ⇒ σ expr → σ expr
current < expr1 >
( [ ] [ ] ) ( [ ] )
σ expr1.Clock → σ[true],σ expr1 → σ[m] ⇒ σ expr → σ[m]