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

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

表 2 右值表达式求值规则

序号 求值规则
R1 (c,σ i−1 , s i ,i) ⇓ c
l
l
(la,σ i−1 , s i ,i) ⇒ s (x)
R2 i
r
(la,σ i−1 , s i ,i) ⇓ s (x)
i
l
(la,σ i−1 , s i ,i) ⇒ (bl,δ)
R3
(&la,σ i−1 , s i ,i) ⇓ ptr(bl,δ)
(ra,σ i−1 , s i ,i) ⇓ v 1
R4 其中,v = (τ)v 1
((τ)ra,σ i−1 , s i ,i) ⇓ v
l
R5 (ra,σ i−1 , s i ,i) ⇓ v (id,σ i−1 , s i ,i) ⇒ (bl,δ) )其中,τ为id[ra]的类型
(
(id[ra],σ i−1 , s i ,i) ⇓ ptr bl,δ+v·sizeof(τ)
l
R6 (ra 1 ,σ i−1 , s i ,i) ⇓ v 1 (ra 2 ,σ i−1 , s i ,i) ⇓ v 2 (id,σ i−1 , s i ,i) ⇒ (bl,δ) 其中,n表示数组id的列数,τ为id[ra 1 ][ra 2 ]的类型
(id[ra 1 ][ra 2 ],σ i−1 , s i ,i) ⇓ ptr(bl,δ+(v 1 ·n+v 2 )· sizeof (τ))
type(la) = struct id{φ} field_offset(v φ ,φ) = δ ′
R7
(la.v φ ,σ i−1 , s i ,i) ⇓ ptr(bl,δ+δ )
′
(ra 1 ,σ i−1 , s i ,i) ⇓ v 1
R8 其中,v = mop 1 v 1
(mop 1 ra 1 ,σ i−1 , s i ,i) ⇓ v
(ra 1 ,σ i−1 , s i ,i) ⇓ v 1 (ra 2 ,σ i−1 , s i ,i) ⇓ v 2
R9 其中,v = v 1 mop 2 v 2
(ra 1 mop 2 ra 2 ,σ i−1 , s i ,i) ⇓ v
(b,σ i−1 , s i ,i) ⇓ true (ra 1 ,σ i−1 , s i ,i) ⇓ v 1
R10
(if (b)then ra 1 else ra 2 ,σ i−1 , s i ,i) ⇓ v 1
(b,σ i−1 , s i ,i) ⇓ false (ra 2 ,σ i−1 , s i ,i) ⇓ v 2
R11
(if (b)then ra 1 else ra 2 ,σ i−1 , s i ,i) ⇓ v 2
(ra,σ i−m−1 , s i−m ,i−m) ⇓ v
R12 其中,m ⩽ i
m
(⊝ ra,σ i−1 , s i ,i) ⇓ v
(ra 1 ,σ i−1 , s i ,i) ⇓ v 1 ,...,(ra k ,σ i−1 , s i ,i) ⇓ v k
R13 其中,vs = (v 1 ,...,v k )
((ra 1 ,...,ra k ),σ i−1 , s i ,i) ⇓ vs

表 3 为 MSVL 布尔表达式求值规则.

表 3 布尔表达式求值规则

序号 求值规则
B1 (true,σ i−1 , s i ,i) ⇓ true
B2 (false,σ i−1 , s i ,i) ⇓ false
{
(ra 1 ,σ i−1 , s i ,i) ⇓ v 1 (ra 2 ,σ i−1 , s i ,i) ⇓ v 2 true 如果v 1 mrop v 2 成立
B3 ,v =
(ra 1 mrop ra 2 ,σ i−1 , s i ,i) ⇓ v false 否则
(b,σ i−1 , s i ,i) ⇓ true (b,σ i−1 , s i ,i) ⇓ false
B4
(¬b,σ i−1 , s i ,i) ⇓ false (¬b,σ i−1 , s i ,i) ⇓ true
{
(b 1 ,σ i−1 , s i ,i) ⇓ v 1 (b 2 ,σ i−1 , s i ,i) ⇓ v 2 true 如果v 1 = true且v 2 = true
B5 ,v =
(b 1 ∧b 2 ,σ i−1 , s i ,i) ⇓ v false 否则
{
(b 1 ,σ i−1 , s i ,i) ⇓ v 1 (b 2 ,σ i−1 , s i ,i) ⇓ v 2 true 如果v 1 = true或v 2 = true
B6 ,v =
(b 1 ∨b 2 ,σ i−1 , s i ,i) ⇓ v false 否则

表 4 为 MSVL 语句的等价规则, 其中 ms 为 MSVL 语句. SKIP 处理 skip 语句. UASS 处理下一状态赋值语句.
AND 处理合取语句. NEXT 处理下一状态语句, 〇ms 表示下一状态执行 ms, more 表示当前区间未结束与 ¬empty
等价. alw ms) 可以表示为 □ms. CHOP 处理顺序语句并对其进行简化. IF 将条件语句转化成等价程序. WHL 将
(

循环语句转化成等价的条件语句. PAR 处理了并行语句. 表 5 为 MSVL 真值的语义等价规则, 其中 P m 为 MSVL
语句.