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

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

l
(15) ⇒ p,g,l ⊢ x s ,µ ⇒ addr ∧ p,g,l ⊢ x s ,µ ⇒ v s E-5, (14)
′
′

Solidity 与 MSVL 中的其他变量的位置和值均未发生改变, 因此
∗

(16) ⇒ (la := ra,σ i−1 , s i ,i) → (true,σ i+1 ,∅,i+2) TR2, (9)

(17) ⇒ α ⊢ µ ∼ s i+1 (3, 5, 7, 10, 15)
′
′
(18) ⇔ P(le = e;,µ,µ ,Normal) TER, (16, 17)

6) 对于 Solidity 单目运算中的自增操作“ ++e; ”, 规则 (E-11) 处理自增表达式, 语句同理, 在 Solidity 中有:
l
(1) p,g,l ⊢ e,µ ⇒ addr ∧ p,g,l ⊢ e,µ ⇒ v E-1, E-9
(2) store(S,addr, sizeof (τ s ),v+1) = S 1 假设
(3) ⇒ p,g,l ⊢ ++e,µ ⇒ Normal,µ 1 E-11, (1, 2)

l
(4) ⇒ p,g,l ⊢ e,µ 1 ⇒ addr ∧load(S 1 ,addr, sizeof (τ s )) = v+1 E-5, (3)

(5) ⇒ µ σ = (µ,µ 1 ) 定义5, (4)
对于 Solidity 赋值运算“ e = e+1 ”, 规则 (E-9) 处理赋值表达式, 语句同理, 在 Solidity 中有:
l
(6) p,g,l ⊢ e,µ ⇒ addr ∧ p,g,l ⊢ e,µ ⇒ v E-1, E-9
(7) store(S,addr, sizeof (τ s ),v+1) = S 假设
′
1
′
(8) ⇒ p,g,l ⊢ e = e+1,µ ⇒ Normal,µ E-9, (6, 7)

1
l ( )

(9) ⇒ p,g,l ⊢ e,µ ⇒ addr ∧load S ,addr, sizeof (τ s ) = v+1 E-5, (8)
′
′
1
1
(10) ⇒ µ = (µ,µ ) 定义5, (9)

′
′
σ 1
自增语句和赋值语句操作均从 Solidity 状态 µ 出发, 得到 µ 1 与 , Solidity 中只有变量 e 的值发生改变, 其他
µ
′
1
µ 1 = µ .
′
变量的位置和值均未改变, 因此有 1
( )
′
′
′
(11) µ | σ= (µ,µ 1 )∧µ | σ = µ,µ ∧µ 1 = µ (5, 10)

1 1

(12) ⇒ (++e;,µ) (e = e+1;,µ) 定义5, (11)
(13) P(e = e+1;,µ,µ ,Normal) 步骤5中已证明
′
(14) ⇒ P(++e;,µ,µ ,Normal) (12, 13)

′
7) 规则 (S-13) 处理 while 循环语句“ while(e) stmt ”, 语句 stmt 正常执行结束, 不存在 return 语句或是执行失
败, 经过 SOL2M 转换器, MSVL 中有“ while(b){ms} ”, 其中 b = TranExp(e) ms = TranExp(stmt).
,
(1) α ⊢ e∼ e b 定理1
(2) α ⊢ µ ∼ s i 已知条件
(3) p,g,l ⊢ e,µ ⇒ false 假设

(4) ⇒ (b,σ i−1 , s i ,i) ⇓ false 定义3, 4, (1, 2, 3)
(5) ⇒ ((while(b){ms}),σ i−1 , s i ,i)

{ }
↣ (if (b)then{ms∧more;while(b){ms}}else empty ,σ i−1 , s i ,i) WHL
↣ ((b∧(ms∧more;while(b){ms}))∨(¬b∧empty),σ i−1 , s i ,i) IF
↣ (empty,σ i−1 , s i ,i) B4, F1, T1, F2, (4)
→ (true,σ i ,∅,i+1)∧(α ⊢ µ ∼ s i ) TR2, (2)

(6) ⇔ P(while(e) stmt,µ,µ ,Normal) TER, (5)
′

8) 规则 (S-14) 同样处理 while 循环语句“ while(e) stmt”, 语句 stmt 正常执行结束, 经过 SOL2M 转换器,
MSVL 中有“ while(b){ms} ”, 其中 b = TranExp(e) ms = TranExp(stmt).
,
(1) α ⊢ e∼ e b 定理1
(2) α ⊢ µ ∼ s i 已知条件
(3) p,g,l ⊢ e,µ ⇒ true∧ p,g,l, f ⊢ stmt,µ ⇒ Normal,µ 1 ∧ P(stmt,µ,µ 1 ,Normal)∧
p,g,l, f ⊢ while(e) stmt,µ 1 ⇒ out,µ 2 ∧ P(while(e) stmt,µ 1 ,µ 2 ,out) 假设