Demo of Formal Methods of Smart Contracts
e-shopping.pml is a simple e-shopping contract program build by PROMELA, and we verify this contract by iSpin.
Detail Process:
- build e-shopping contract program
- install iSpin follow the guide of How to install iSpin
- use iSpin to verify our contract program（Using iSpin）
- ispin e-shopping.pml
- click 'Syntax Check'： check our program
- click 'Simulate/Replay' -> (Re)Run： run check
- result dialog will show the check result
- finally, our check result was recorded in 'result.png'