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

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

p,g,l ⊢ e,µ ⇒ v is_true(v,τ v ) p,g,l, f ⊢ stmt,µ ⇒ Normal,µ 1
(S-14)
p,g,l, f ⊢ while(e) stmt,µ 1 ⇒ out,µ 2
p,g,l, f ⊢ while(e) stmt,µ ⇒ out,µ 2

p,g,l ⊢ e,µ ⇒ v is_true(v,τ v ) p,g,l, f ⊢ stmt,µ ⇒ out,µ 1 out = Return|Fail
(S-15)
p,g,l, f ⊢ while(e) stmt,µ ⇒ out,µ 1
while 循环语句其实质与 for 循环类似, 只是缺少了初始化语句. 因此给出 3 个不同的规则, 根据终止条件的评
估结果使用相应的规则. 当循环条件 e 的求值规则 为 v false 时, while 循环结束, 参考规则 (S-13). 当循环条件 e 的
v 为 stmt 正常执行结束, 得到新的状态 , 并继
求值规则 true 时, 执行循环内的语句 stmt, 并产生语句执行结果, 当 µ 2
续执行循环语句, 得到最终状态 µ 3 , 参考规则 (S-14). 当 stmt 为 return 语句或引发异常时, 循环立即终止, 状态不再
发生改变, 参考规则 (S-15).
函数调用语句可分为两类: 内部调用和外部调用. 内部调用是指同一合约函数之间的调用, 外部调用是指不同
合约函数之间的调用.
此处需引入新的语义元素:
● C: 区块链中定义的所有智能合约标识符的集合.
● G: 从智能合约标识符映射到各自全局变量的函数.
( )
● fundef g,id c ,id f 函数有 3 个参数: 合约名称和需要调用的函数名称, 若函数 id f 存在, 则 fundef 函数返回其
函数定义, 记为 func, 否则返回 ∅.
内部函数调用的操作语义:

(
)
∗ fundef g,id c ,id f = func and func , ∅
p,g,l ⊢ e ,µ ⇒ vs,µ 1
(S-16)
p,g,l, f ⊢ func(vs),µ 1 ⇒ v re ,µ 2
∗
p,g,l, f ⊢ id f (e ),µ ⇒ v re ,µ 2

)
(
∗ fundef g,id c ,id f = ∅
p,g,l ⊢ e ,µ ⇒ vs,µ 1
(S-17)
p,g,l, f ⊢ id f (vs),µ 1 ⇒ Fail,µ 2
∗
p,g,l, f ⊢ id f (e ),µ ⇒ Fail,µ 2
内部函数调用时, 首先对函数的参数列表进行求值, 之后检查函数在该智能合约中是否存在定义, 若存在, 执
行函数代码, 函数分为有返回值和无返回值两类, 在此不过多赘述. 若函数在该合约中不存在定义, 则执行结果为
Fail.
( )
外部函数调用的形式为: e 1 .e 2 e , 其中 e 1 表示外部合约, e 2 表示需调用的外部函数. 首先需要从区块链中获
∗
3
取外部合约的信息, 判断需调用的函数是否存在, 若存在, 则执行函数, 否则调用失败, 此时 Solidity 会自动调用其
回退函数 fallback, 回退函数涉及到区块链操作, 在 MSVL 中没有相对应的描述, 因此这里使用 Fail 表示外部函数
调用失败.
外部函数调用的操作语义:

∗
p,g,l ⊢ e 1 ,µ ⇒ id c ,µ 1 p,g,l ⊢ e 2 ,µ 1 ⇒ id f ,µ 2 p,g,l ⊢ e ,µ 2 ⇒ vs,µ 3
3
id c < C p,g,l, f ⊢ id c .id f (vs),µ 3 ⇒ Fail,µ 4 (S-18)
( )
∗
p,g,l, f ⊢ e 1 .e 2 e ,µ ⇒ Fail,µ 4
3
∗
p,g,l ⊢ e 1 ,µ ⇒ id c ,µ 1 p,g,l ⊢ e 2 ,µ 1 ⇒ id f ,µ 2 p,g,l ⊢ e ,µ 2 ⇒ vs,µ 3
3
)
(
fundef g c ,id c ,id f = func and func , ∅
id c ∈ C G(id c ) = g c
(S-19)
p,g,l, f ⊢ id c .func(vs),µ 3 ⇒ v re ,µ 4
( )
∗
p,g,l, f ⊢ e 1 .e 2 e ,µ ⇒ v re ,µ 4
3
∗
p,g,l ⊢ e 1 ,µ ⇒ id c ,µ 1 p,g,l ⊢ e 2 ,µ 1 ⇒ id f ,µ 2 p,g,l ⊢ e ,µ 2 ⇒ vs,µ 3
3
fundef g c ,id c ,id f = ∅
(
)
id c ∈ C G(id c ) = g c
(S-20)
p,g,l, f ⊢ id c .id f (vs),µ 3 ⇒ Fail,µ 4
( )
∗
p,g,l, f ⊢ e 1 .e 2 e ,µ ⇒ Fail,µ 4
3