 |
The properties derived from the functional requirements of the smart contract were converted to TCTL.
Property 1 states that if the deduction time interval specified by the beneficiary and the clock of the contract template becomes the same, the current proposed price is the same as the price reduced by the deduction amount from the initial proposed price.
In this property, the 'count' variable represents the number of times the amount has been decreased. And when the clock of the contract template becomes equal to the deduction time interval, it is initialized to 0.
Property 2 states that if the bidder in the bidding state is bidder(i) and bidder(j), it means that i and j are the same, indicating that it cannot exist in the bidding state at the same time.
property 3 is a safety property, and it has been shown that the initial proposed price does not deducted below the lowest proposed price in all states of all routes. |
IEEE/ICACT20210216 Slide.14
[Big Slide]