Page 107 - 《软件学报》2025年第9期

4018 软件学报 2025 年第 36 卷第 9 期

句有 3 种情况: 无返回值 (S-2), 返回一个值 (S-3), 返回值列表 (S-4). return 语句的操作语义如下:

p,g,l, f ⊢ return;,µ ⇒ Return,µ ′ (S-2)

p,g,l ⊢ e,µ ⇒ v
(S-3)
p,g,l, f ⊢ return e,µ ⇒ Return v,µ ′

p,g,l ⊢ e ,µ ⇒ vs
∗
(S-4)
p,g,l, f ⊢ return e ,µ ⇒ Return vs,µ ′
∗
e 的真值选择执行哪一部分的语句, 因此执行前后状态发生变化, if 语句的操
条件语句根据条件判断表达式
作语义如下:

p,g,l ⊢ e,µ ⇒ v is_true(v,τ v ) p,g,l, f ⊢ stmt 1 ,µ ⇒ out,µ ′
(S-5)
p,g,l, f ⊢ if (e) stmt 1 (else stmt 2 ),µ ⇒ out,µ ′

p,g,l ⊢ e,µ ⇒ v is_ false(v,τ v ) p,g,l, f ⊢ stmt 2 ,µ ⇒ out,µ ′
(S-6)
p,g,l, f ⊢ if (e) stmt 1 (else stmt 2 ),µ ⇒ out,µ ′
e
首先对条件判断表达式进行求值, 其中 is_true(v,τ) 与 is_false(v,τ) 函数用于描述判定条件 的求值结果. 当
求值结果为 true 时, 执行第 1 个分支的语句 stmt 1 , 得到语句 stmt 1 的执行结果 out, 条件语句的执行结果与语句
stmt 1 的结果一致, 参考规则 (S-5). 当判定条件求值结果为 false 时, 条件语句的执行结果与语句 stmt 2 的结果一致,
参考规则 (S-6).
顺序执行语句的操作语义如下:

p,g,l, f ⊢ stmt 1 ,µ ⇒ Normal,µ 1 p,g,l, f ⊢ stmt 2 ,µ 1 ⇒ out,µ 2
(S-7)
p,g,l, f ⊢ stmt 1 ; stmt 2 ,µ ⇒ out,µ 2

p,g,l, f ⊢ stmt 1 ,µ ⇒ Fail|Return,µ ′
(S-8)
p,g,l, f ⊢ stmt 1 ; stmt 2 ,µ ⇒ Fail|Return,µ ′
当第 1 个语句 stmt 1 正常执行结束时, 顺序执行语句的执行结果与 stmt 2 的执行结果一致, 参考规则 (S-7). 当
stmt 1 执行失败或者包含 return 语句时, stmt 1 一致, 参考规则 (S-8).
语句 stmt 2 不再执行, 顺序执行语句的执行结果与
循环语句有两类, 其语法定义如下:
(1) While(e) stmt
(2) for(stmt 1 ;e;stmt 2 ) stmt
for 循环语句的操作语义:

p,g,l, f ⊢ stmt 1 ,µ ⇒ Normal,µ 1 p,g,l, f ⊢ for(;e; stmt 2 ) stmt,µ 1 ⇒ out,µ 2
(S-9)
p,g,l, f ⊢ for(stmt 1 ;e; stmt 2 ) stmt,µ ⇒ out,µ 2

p,g,l ⊢ e,µ ⇒ v is_false(v,τ v )
(S-10)
p,g,l, f ⊢ for(;e; stmt 2 ) stmt,µ ⇒ out,u

p,g,l ⊢ e,µ ⇒ v is_true(v,τ v ) p,g,l, f ⊢ stmt,µ ⇒ Normal,µ 1
(S-11)
p,g,l ⊢ stmt 2 ,µ 1 ⇒ out,u 2 for(;e; stmt 2 ) stmt,µ 2 ⇒ out,µ 3
p,g,l, f ⊢ for(;e; stmt 2 ) stmt,µ ⇒ out,µ 3

p,g,l ⊢ e,µ ⇒ v is_true(v,τ v ) p,g,l, f ⊢ stmt,µ ⇒ out,µ 1 out = Return|Fail
(S-12)
p,g,l, f ⊢ for(;e; stmt 2 ) stmt,µ ⇒ out,µ 1
stmt 1 ; for(;e; stmt 2 ) stmt, 参考规
for 循环语句首先执行初始化语句 stmt 1 , 再执行循环内容, 因此可将其拆分为
则 (S-9), 根据终止条件给出 3 个循环规则. 循环判断条件 e 1 求值为 false 时, 循环结束, 参考规则 (S-10). 循环条件
e 1 值为 true 时, 先执行循环体内语句 stmt, 正常执行完毕后, 再执行 , 得到新的状态, 从新的状态出发, 继续进入
e 2
循环, 参考规则 (S-11). 若循环体内语句执行结果为 Return 或 Fail, 表明函数在此处返回或者出现异常, 循环立刻
结束, 参考规则 (S-12).
while 循环函数的操作语义:

p,g,l ⊢ e,µ ⇒ v is_ false(v,τ v )
(S-13)
p,g,l, f ⊢ while(e) stmt,µ ⇒ out,µ