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

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

(1) α ⊢ e∼ e l 归纳假设
(2) α ⊢ µ ∼ s 已知条件
(3) p,g,l ⊢ le[e],µ ⇒ v s ∧(id[ra].right,σ, s,|σ|+1) ⇓ v m 假设
(4) ⇒ p,g,l ⊢ e ⇒ v s1 ∧v s = map(v s1 ) E-7, (3)

(5) ⇒ (id m [ra].le ft,σ, s,|σ|+1) ⇓ v m1 ∧(l,σ, s,|σ|+1) ⇓ v m2 ∧v m = map(v m1 ) L2, R7, (4)

(6) ⇒ v s1 = v m2 ∧v m1 = v m2 V1, (1, 2, 4, 5)
(7) ⇒ v s1 = v m1 (6)

(8) ⇒ α ⊢ map(v s1 ) ∼ map(v m1 )∧v s = map(v s1 )∧v m = map(v m1 ) V3, (4, 5, 7)

(9) ⇒ α ⊢ v s ∼ v m (8)

(10) ⇔ α ⊢ le[e]∼ r id[ra].right 定义3, (9)

(11) ⇒ α ⊢ le[e]∼ e id[ra].right 定义4, (10)
自增自减表达式和赋值表达式将在下一节中作为赋值语句给出赋值语句等价性证明.

3.4 语句等价性证明
定理 2. 通过 SOL2M 转换器, 将 Solidity 语句 stmt 转换为 MSVL 语句 ms, 记为 ms = TranStmt(stmt). 对于任
意给定的内存注入 α, 任意的 µ ∈ S, s i ∈ M, 如果 α ⊢ µ ∼ s i , 那么有 α ⊢ stmt∼ s ms.

证明: 本文采用规则归纳法对定理进行证明, 设 P 为性质.
( )
∗
′ ′ (TER)
P(stmt,µ,µ ,out) ⇔ α ⊢ µ ∼ s i ⇒ (ms,σ i−1 , s i ,i) → (true,σ,∅,|σ|+1)∧α ⊢ µ ∼ s |σ|
施规则归纳于命令去证明

p,g,l, f ⊢ stmt,µ ⇒ out,µ ⇒ P(stmt,µ,µ ,out).
′
′
以下是具体证明过程. 归纳奠基:
1) 规则 (S-1) 处理空语句‘;’, 结论显然成立.
2) 规则 (S-5) 和 (S-6) 处理条件语句“ if (e) stmt 1 else stmt 2 ”. TranStmt(if (e) stmt 1 else stmt 2 ) = “if(b) then {ms 1 }
,
,
else {ms 2 }”, 其中 b = TranExp(e) ms 1 = TranStmt(stmt 1 ) ms 2 = TranStmt(stmt 2 ).
对于规则 (S-5), 其中 b 求值为 true, 其证明如下:
(1) α ⊢ e∼ e b 定理1
(2) α ⊢ µ ∼ s i 已知条件
(3) p,g,l ⊢ e,µ ⇒ true∧ p,g,l, f ⊢ stmt 1 ,µ ⇒ out ,µ ∧ P(stmt 1 ,µ,µ ,out) 归纳假设
′
′
′
∗
(4) ⇔ (ms 1 ,σ i−1 , s i ,i) → (true,σ,∅,|σ|+1)∧α ⊢ µ ∼ s |σ| TER, (2, 3)

′
(5) ⇒ (b,σ i−1 , s i ,i) ⇓ true 定义3, 4, (1, 2, 3)

(6) ⇒ (if (b) then {ms 1 } else {ms 2 },σ i−1 , s i ,i)

↣ ((b∧ms 1 )∨(¬b∧ms 2 ),σ i−1 , s i ,i) IF
↣ (ms 1 ,σ i−1 , s i ,i) B4, T1, F1, F2, (5)
∗
→ (true,σ,∅,|σ|+1)∧(α ⊢ µ ∼ s |σ| ) (4)
′

(7) ⇔ P(if (e) stmt 1 else stmt 2 ,µ,µ ,out) TER, (6)
′
对于规则 (S-6), 其中 b 求值为 false, 其证明如下:
(1) α ⊢ e∼ e b 定理1
(2) α ⊢ µ ∼ s i 已知条件
′
′
(3) p,g,l ⊢ e,µ ⇒ false∧ p,g,l, f ⊢ stmt 2 ,µ ⇒ out,µ ∧ P(stmt 2 ,µ,µ ,out) 归纳假设
∗

(4) ⇔ (ms 2 ,σ i−1 , s i ,i) → (true,σ,∅,|σ|+1)∧α ⊢ µ ∼ s |σ| TER, (2, 3)
′
(5) ⇒ (b,σ i−1 , s i ,i) ⇓ false 定义3, 4, (1, 2, 3)

(6) ⇒ (if (b)then{ms 1 }else{ms 2 },σ i−1 , s i ,i)