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

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

′
ext f (ra 1 ,...,ra k ,RVal)},σ i−1 , s i ,i) → (P m ,σ i , s i+1 ,i+1) 且 s i+1 = s .
n
ext g(ra 1 ,...,ra k ) 类似于黑盒调用, 其规则如下.
外部函数
)
● EXT2. 如果对每个 1 ⩽ j ⩽ k, ( ra j ,σ i−1 , s i ,i ⇓ v j , 且 < s i > 是 g(v 1 ,...,v k ) 的模型, 那么 (∧{〇P m ,ext g(ra 1 ,...,
,
ra k )},σ i−1 , s i ,i) → (P m ,σ i , s i+1 ,i+1) s i+1 = s i . 这表示 g(ra 1 ,...,ra k ) 在一个单独的状态 s i 上执行, 将其插入主区间 .
σ i

2 Solidity 语法与操作语义
本节首先回顾 Solidity 语法, 随后对其操作语义进行了定义, 其中对 Solidity 的形式化定义侧重于动态语义,
为 Solidity 语言定义了状态与语义元素, 在全局环境上与局部环境上定义了相关操作, 以大步语义的形式制定了
Solidity 的求值规则, 分为左值表达式、右值表达式以及语句的求值规则, 并根据 Solidity 语法, 给出了表达式与语
句的操作语义.

2.1 Solidity 语法
Solidity 的语法接近于 JavaScript, 相比于高级程序设计语言, 缺少多线程以及高并发等特性. Solidity 的表达
式归纳定义如下.

le ::= id|le[e]|le.id

( )
e ::= constant|id|le[e]|le.e|e 1 e |e |unop e|e 1 binop e 2 |le assign e
∗
∗
2
unop ::= ++|−−|!| ∼ bop 1 ::= +|−|∗|/|%

bop ::=<< | >> |&| || ∧ bop ::=== |! =
2 3

bop ::=> | >= | < | <= bop ::= &&| ∥
4 5
binop ::= bop 1 |bop 2 |bop 3 |bop 4 |bop 5

assign ::== |+ = |− = |∗ = |/ =
其中, le 表示左值表达式, 可以通过寻址操作获取其内存地址, id 为变量名称; e 为表达式, 包括常量 constant, 变量
( )
id, 数组元素, 结构体成员等, e 1 e ∗ 2 表示函数调用, e 表示元组; unop 表示单目运算, 包括自增 ( ++), 自减 ( −−), 逻
∗
辑非 (!) 和位运算符 ( ∼); binop 表示双目运算, 包括算术运算符记为 bop 1 , 位运算符记为 bop 2 , 关系运算符记为
bop 4 , 以及逻辑运算符 ( bop assign 表示赋值表达式.
;
bop 3 和 &&,∥), 记为
5
Solidity 程序的相关定义如下:

limit ::= publicprivateinternal

location ::= memory|storage

type ::= uint8|uint16|uint32|uint64|uint128|uint256|address|bool

mapping(type 1 => type 2 )id t |type[]

∗
StructDef ::= struct id{(type id) }

VarDe f ::= type location? id

∗
FunDe f ::= function id(VarDe f )limit?FunReturn?stmt

FunReturn ::= returns((type id) )
∗

Block ::= StructDef |VarDe f|FunDe f

P s ::= contract id c {Block}
其中, limit 表示可见性关键词 public (任何用户或者合约都能调用和访问), private (只能在其所在的合约中调用和
访问), internal (子合约可以访问父合约中定义的 internal 函数); location 表示数据内存类型 memory (存储于函数内
部) 和 storage (存储于函数外部); type 表示 Solidity 中的数据类型, 包含: uint8–uint256, 地址类型 address (表示区
块链中的合约地址), 布尔类型 bool, 映射类型 mapping, 自定义类型 id t 以及数组. StructDef 表示结构体定义,
VarDe f 表示变量定义, FunDe f 表示函数定义, FunReturn 表示函数返回定义. P s 表示 Solidity 程序, 由关键字
contract、合约名称与合约体 Block 组成, 合约体 Block 包含结构体定义、变量定义与函数定义.