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

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

表 4 语句等价规则

序号 等价规则
SKIP skip ≡ 〇empty
l
UASS 如果(la,σ i−1 , s i ,i) ⇒ s (x),且(ra,σ i−1 , s i ,i) ⇓ n,那么la := ra ≡ 〇(x ⇐ n∧empty)
l
i
AND ms 1 and ms 2 ≡ ∧{ms 1 ,ms 2 }
NEXT next ms ≡ ∧{〇ms,more}
{ } { }
(1)∧ □ms,empty ≡ ∧ ms,empty
ALW
(2)∧{□ms,more} ≡ ∧{ms,〇□ms}
(1)∧{w,ms 1 };ms 2 ≡ ∧{w,ms 1 ;ms 2 }
CHOP (2)〇ms 1 ;ms 2 ≡ 〇(ms 1 ;ms 2 )
(3)empty;ms 2 ≡ ms 2
(4)□more;ms 2 ≡□more

IF if (b)then{ms 1 }else{ms 2 } ≡ (b∧ms 1 )∨(¬b∧ms 2 )
{ }
WHL while(b){ms} ≡ if (b)then{ms∧more;while(b){ms}}else empty
PAR ms 1 ∥ ms 2 ≡ ∨{∧{ms 1 ; true, ms 2 },∧{ms 1 ,ms 2 ; true },∧{ms 1 ,ms 2 }}

表 5 真值的语义等价规则

序号 等价规则
F1 ∧{false,P m } ≡ false
F2 ∨{P m ,false} ≡ P m
F3 ∧{P m ,¬P m } ≡ false
T1 ∧{true,P m } ≡ P m
T2 ∨{P m ,true} ≡ true
T3 ∨{P m ,¬P m } ≡ true

MSVL 赋值语句规则如下.
( ) l l ( ) ( ) n
● MIN1. 如果 ∃j,1 ⩽ j ⩽ n, la j ,σ i−1 , s i ,i ⇒ s x j 且 ra j ,σ i−1 , s i ,i ⇓ v j , 那么 (∧{P m ,∧ {la k ⇐ ra k }},σ i−1 , s i ,i) ↣
i k=1
n l r
(∧{P m ,∧ {la k [v j /x j ]}},σ i−1 ,(s , s [v j /x j ]),i).
k=1,k, j i i
l ( ) la j ⇐ ra j 从该格局中
变量 x j 的存储位置 la j 求左值得到 s x j , 变量 x j 的值 ra j 求值得到 . 将立即赋值语句
v j
i
删除并将 s i 状态下的变量 x j 的值设置为 v j (1 ⩽ k ⩽ n且k , j).
l
l
● MIN2. 如果 (⊝x,σ i−1 , s i ,i) ⇓ v, 并且在程序 P m 中没有语句 la ⇐ ra, 其中, (la,σ i−1 , s i ,i) ⇒ s (x), 那么 (P m ,σ i−1 ,
i
l r
s i ,i) ↣ (P m ,σ i−1 ,(s , s [v/x]),i). 如果当前状态下未对变量 x 进行赋值, 则其值与上一状态保持一致.
i
i
〇ms 或者 empty. 其求值规则如下.
当前状态下所有变量都被设置后, 程序简化为
( )
● TR1. 〇ms,σ i−1 , s i ,i → (ms,σ i , s i+1 ,i+1)
( )
● TR2. empty,σ i−1 , s i ,i → (true,σ i ,∅,i+1)
MSVL 函数调用可分为外部调用和内部调用 [17] . 执行外部调用时, 程序 P m 的前后时序状态区间可认为未发
生变化, 执行内部调用时, 程序 P m 正常记录时序状态区间的变化. MSVL 函数调用求值规则如下.
(1) 内部调用, 对于 function f (τ 1 x 1 ,...,τ k x k ,τ RVal){mdcl;ms}, 其中 mdcl 是函数内部变量定义语句. 求值规则
如下.
k
● FUN. f(ra 1 ,...,ra k ,RVal) ≡ ((∧ τ j x j ⇐ ra j ∧mdcl);ms;)
j=1

〇(ext mfree(x 1 ,..., x k ,RVal,mdcl)∧empty),
其中, mfree(x 1 ,..., x k ,RVal,mdcl) 是一个用于释放变量和内存的外部函数.
(2) 外部函数调用, 仅关注执行前后的信息. 分为用户定义函数和外部函数两种.
用户定义函数 ext f(ra 1 ,...,ra k ,RVal) 类似于白盒调用, 其规则如下.
+
′ ′ ′ ′ k ′ ′
,
● EXT1. 如果 σ =< s ,..., s > s = s i 且 ((∧ τ j x j ⇐ ra j ∧mdcl);ms,ϵ, s ,0) → (true,σ ,∅,n+1), 那么, (∧{〇P m ,
0 n 0 j=1 0