Refactor to increase readability

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";
 }
 
 

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()";
 }
 
 

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];
 	}