diff --git a/02.Lesson_InvestigateViolations/ERC20/ERC20.spec b/02.Lesson_InvestigateViolations/ERC20/ERC20.spec index c0aa40da..78e08920 100644 --- a/02.Lesson_InvestigateViolations/ERC20/ERC20.spec +++ b/02.Lesson_InvestigateViolations/ERC20/ERC20.spec @@ -11,8 +11,10 @@ rule integrityOfTransfer(address recipient, uint256 amount) { uint256 balanceSenderBefore = balanceOf(e, e.msg.sender); uint256 balanceRecipientBefore = balanceOf(e, recipient); transfer(e, recipient, amount); + uint256 balanceSenderAfter = balanceOf(e, e.msg.sender); + uint256 balanceRecipientAfter = balanceOf(e, recipient); - assert balanceRecipientBefore + balanceSenderBefore == balanceOf(e, e.msg.sender) + balanceOf(e, recipient), "the total funds before and after a transfer should remain the constant"; + assert balanceRecipientBefore + balanceSenderBefore == balanceRecipientAfter + balanceSenderAfter, "the total funds before and after a transfer should remain constant"; } diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec index 735f9f05..46ec057c 100644 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec @@ -53,8 +53,10 @@ rule checkStartedToStateTransition(method f, uint256 meetingId) { calldataarg args; uint8 stateBefore = getStateById(e, meetingId); f(e, args); - assert (stateBefore == 2 => (getStateById(e, meetingId) == 2 || getStateById(e, meetingId) == 4)), "the status of the meeting changed from STARTED to an invalid state"; - assert ((stateBefore == 2 && getStateById(e, meetingId) == 4) => f.selector == endMeeting(uint256).selector), "the status of the meeting changed from STARTED to ENDED through a function other then endMeeting()"; + uint8 stateAfter = getStateById(e, meetingId); + + assert (stateBefore == 2 => (stateAfter == 2 || stateAfter == 3)), "the status of the meeting changed from STARTED to an invalid state"; + assert ((stateBefore == 2 && stateAfter == 3) => f.selector == endMeeting(uint256).selector), "the status of the meeting changed from STARTED to ENDED through a function other then endMeeting()"; } @@ -67,9 +69,11 @@ rule checkPendingToCancelledOrStarted(method f, uint256 meetingId) { uint8 stateBefore = getStateById(e, meetingId); f(e, args); - assert (stateBefore == 1 => (getStateById(e, meetingId) == 1 || getStateById(e, meetingId) == 2 || getStateById(e, meetingId) == 4)), "invalidation of the state machine"; - assert ((stateBefore == 1 && getStateById(e, meetingId) == 2) => f.selector == startMeeting(uint256).selector), "the status of the meeting changed from PENDING to STARTED through a function other then startMeeting()"; - assert ((stateBefore == 1 && getStateById(e, meetingId) == 4) => f.selector == cancelMeeting(uint256).selector), "the status of the meeting changed from PENDING to CANCELLED through a function other then cancelMeeting()"; + uint8 stateAfter = getStateById(e, meetingId); + + assert (stateBefore == 1 => (stateAfter == 1 || stateAfter == 2 || stateAfter == 4)), "invalidation of the state machine"; + assert ((stateBefore == 1 && stateAfter == 2) => f.selector == startMeeting(uint256).selector), "the status of the meeting changed from PENDING to STARTED through a function other then startMeeting()"; + assert ((stateBefore == 1 && stateAfter == 4) => f.selector == cancelMeeting(uint256).selector), "the status of the meeting changed from PENDING to CANCELLED through a function other then cancelMeeting()"; } diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol b/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol index cce3d0a8..e356dcc8 100644 --- a/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol @@ -101,7 +101,7 @@ contract AuctionImpl is TokenInterface { require(auctions[id].bid_expiry != 0 && (auctions[id].bid_expiry < now || auctions[id].end_time < now)); - mint(auctions[id].winner, auctions[id].prize);n + mint(auctions[id].winner, auctions[id].prize); delete auctions[id]; }