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

王小兵 等: Solidity 到 MSVL 转换的等价性研究 4029

∗ ( )
(4) ⇔ ((ms,σ i−1 , s i ,i) → true,σ j ,∅, j+1 ∧α ⊢ µ 1 ∼ s j )∧

( ) ∗
while(b){ms},σ j−1 , s j , j → (true,σ,∅,|σ|+1)∧α ⊢ µ 2 ∼ s |σ| TER, (3)
(5) ⇒ (b,σ i−1 , s i ,i) ⇓ true 定义3, 4, (1)

(6) ⇒ ((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

↣ (ms∧more;while(b){ms},σ i−1 , s i ,i) B4, F1, T1, F2, (4)
∗
→ (empty;while(b){ms},σ j−1 , s j , j) (4)

↣ (while(b){ms},σ j−1 , s j , j) CHOP
∗
→ (true,σ,∅,|σ|+1)∧(α ⊢ µ 2 ∼ s |σ| ) (4)

(7) ⇔ P(while(e) stmt,µ,µ ,Normal) TER, (6)
′
9) 规则 (S-15) 同样处理 while 循环语句“ while(e) stmt ”, 如果语句 stmt 包含无返回值的 return 语句, 经过
,
SOL2M 转换器, MSVL 中有“ while(b and rflag = 0){ms} ”, 其中 b = TranExp(e) ms = TranExp(stmt),rflag 初始值
为 0, 表示当前未出现 return 语句.
(1) α ⊢ e∼ e b 定理1
(2) α ⊢ µ ∼ s i 已知条件
(3) p,g,l ⊢ e,µ ⇒ true∧ p,g,l, f ⊢ stmt,µ ⇒ Return,µ 1 ∧ P(stmt,µ,µ 1 ,Return) 假设
∗ ( )

(4) ⇔ (ms,σ i−1 , s i ,i) → true,σ j ,∅, j+1 ∧α ⊢ µ ∼ s j TER, (2, 3)
′

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

(6) ⇒ (b∧rflag = 0,σ i−1 , s i ,i) ⇓ true B3, B5, (5)

(7) ⇒ (while(b and rflag = 0){ms},σ i−1 , s i ,i)
∗
↣ ((b∧rflag = 0∧(ms∧more;while(b∧rflag = 0){ms})∨
¬(b∧rflag = 0)∧empty),σ i−1 , s i ,i) WHL, IF
↣ (ms∧more;while(b∧rflag = 0){ms},σ i−1 , s i ,i) B4, F1, T1, F2, (6)

∗
→ (∧{empty,rflag ⇐ 1};while(b∧rflag = 0){ms},σ j−1 , s j , j) (3, 4)
↣ (empty;while(b∧rflag = 0){ms},σ j−1 , s j [1/rflag], j) MIN1
↣ (while(b∧rflag = 0){ms},σ j−1 , s j , j) CHOP
∗
↣ ((b∧rflag = 0∧(ms∧more;while(b∧rflag = 0){ms})∨
¬(b∧rflag = 0)∧empty),σ j−1 , s j , j) WHL, IF
↣ (empty,σ j−1 , s j , j) F1, T1, F2
(
)
′
→ true,σ j ,∅, j+1 ∧(α ⊢ µ ∼ s j ) (4)
(8) ⇔ P(while(e) stmt,µ,µ ,Return) TER, (7)

′
同理可证得含有返回值的 return 语句.
10) 规则 (S-9) 至 (S-12) 处理 for 循环语句“ for(stmt 1 ;e; stmt 2 ) stmt ”. 根据规则 (S-9) 与定义 5, 执行语句 stmt 1
后得到状态 µ 1 , 执行“ for(;e; stmt 2 ) stmt ”后得到状态 , 显然可知 (for(stmt 1 ;e; stmt 2 ) stmt) (stmt 1 ;for(;e; stmt 2 )
µ 2
stmt). 根据规则 (S-10) 至 (S-12) 可知 (for(;e; stmt 2 ) stmt) (while(e){ stmt; stmt 2 }). 因此有 (for(stmt 1 ;e; stmt 2 )stmt)
(stmt 1 ;while(e){stmt; stmt 2 }), 则 for 循环语句的等价性证明可由步骤 9 证明.
11) 规则 (S-16) 与 (S-21) 处理内部函数调用语句“ id f (e ) ”, 在 MSVL 中有“ f (ra ,RVal) = TranStmt(e 1 (e )),
∗
∗
∗
”
2
( )
∗
其中, f = TranExp id f , ra = TranExp(e ) e = (e 1 ,...,e k ) ra = (ra 1 ,...,ra k ), 且 e i = TranExp(ra i )(1 ⩽ r ⩽ k).
,
∗
∗
∗
,
(1) α ⊢ e ∼ ra 定理1
∗
∗
(2) α ⊢ µ ∼ s i 已知条件