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

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

1 contract voteContract {
2 struct Candidate {
3 bytes8 name;
4 uint voteCount;
5 }
6 uint public winnerId=0;

7 mapping(address=>uint) public voters;
8 Candidate[ ] public candidates;

9 function vote(address sender,uint id) public {
10 if (voters[sender]==0) {
11 return;
12 }else{
13 voters[sender]=voters[sender]-1

14 candidates[id].voteCount=candidates[id].voteCount+1
15 }
16 }

17 function winner(⋅) public {
18 uint maxCount=0;
19 for (uint i=0; i<candidates.length; i++) {

20 if (candidates[i].voteCount>maxCount) {
21 maxCount=candidates[i].voteCount;

22 winnerId=i;
23 }
24 }
25 }
26 }

Fig.12 Vote smart contract
图 12 投票智能合约

Fig.13 Modeling results of SOL2M converter
图 13 SOL2M 转换器建模结果

Table 5 Temporal operators in PPTL
表 5 PPTL 中的时序操作符
操作符 文本表示 操作符 文本表示
¬ ! ∧ and
□ alw ∨ or
〇 next → ->
◇ som fin fin