Page 281 - 《软件学报》2021年第6期

王小兵 等:面向 MSVL 的智能合约形式化验证 1855

〈IDENTIFIER:〈LETTER〉(〈LETTER〉|〈DIGIT〉)*〉

〈LETTER:[“A”−“Z”,“_”,“a”−“z”]〉
〈DIGIT:[“0”−“9”]〉
Fig.5 Regular expressions of identifiers
图 5 标识符的正则表达式
(3) 运算符与界限符
运算符是语言固有的操作符号,Solidity 语言中的运算符见表 2.
Table 2 Operators
表 2 运算符
运算符 对应标记 运算符 对应标记
“+” PLUS “/” DIVIDE
“−” MINUS “*” MULTIPLY
“++” SELFPLUS “−−” SELEFMINUS
“%” REMAINDER “>” GREAT
“<” LOWER “>=” GREATER
“==” EQUAL “!=” UNEQUAL
“<=” LOWERW “!” NOT
“&&” AND “||” OR
“&” BIT_ADD “|” BIT_OR
“^” BIT_XOR “~” BIT_NOT
“=” ASSIGNMENT “+=” PLUS_ASSIGNMENT
“−=” MINUS_ASSIGNMENT “*=” MULTIPLY_ASSIGNMENT
“/=” DIVIDE_ASSIGNMENT “%=” REMAINDER_ASSIGNMENT
“&=” BIT_ADD_ASSIGNMENT “|=” BIT_OR_ASSIGNMENT
“^=” BIT_XOR_ASSIGNMENT “~=” BIT_NOT_ASSIGNMENT

界限符主要用于分割不同语句或标识符,Solidity 中的界限符见表 3.
Table 3 Boundary characters
表 3 界限符
界限符 对应标记 界限符 对应标记
“(” LC “) ” RC
“[” LM “]” RM
“{” LB “}” RB
“.” SPOT “:” COLON
“;” SEMICOLON “,” DOT
(4) 常量
常量为不会发生改变的内容,如整型常量、布尔常量、地址常量和字符常量,这 4 类常量通常能满足大部
分智能合约的要求,如果合约需要更复杂的常量,只需在 JavaCC 的常量定义部分进行扩充,常量的正则表达式
如图 6 所示.
INTEGER_LITERAL:〈HEX_LITERAL〉|〈CONSTANT〉

〈HEX_LITERAL:“hex”([“0”−“9”,“a”−“f”,“A”−“F”])+〉

〈CONSTANT:“0”|[“1”−“9”](〈DIGIT〉)*〉
〈DIGIT:[“0”−“9”]〉
Fig.6 Regular expressions of constants
图 6 常量的正则表达式
3.3 语法分析模块
语法分析建立在词法分析的基础之上,对词法分析生成的单词序列按照语法规则组成有特定含义的语句,
并生成与源代码等价的语法树.本文使用 BNF 范式描述智能合约的语法规则.
首先,智能合约由结构体、状态变量、函数以及事件 4 部分组成,其 BNF 定义如图 7 所示.合约以 Start 为
开始,以 Procedure 为终止.合约主体部分为 ContractBlock 声明,包含 Struct,Statedef 以及 Method,分别用于声明