This document tells you what you will develop, namely "Counter". Although it is quite simple, you'll still need to understand it carefully.
Here is the full specification of the counter system.
The objective of the system is to help the user to count the number of a certain event. We don't care what the event is because this system is a general purpose counter.
For example, a baseball umpire may use this system to count the current number of strikes so that the umpire can correctly call a "strike out". In this senario, the user will reset the counter when a new batter comes in. When the pitcher gives a strike ball, the user increments the counter. If the count value is three, the user should shout out "strike out". The umpire may use this system also for the ball count, but in this case the umpire should use two sets of the counter system so that ball counts and strike counts do not get mixed.
As you see from the signature of the operation inc(), it does not return the new counter value.
So, you'll have to use the operation get() to retrieve the updated value.
The last operation of the system is reset() to reset the counter to 0.
The system has a limited size of memory as well as any other computer systems.
Thus, the value of count should not exceed 9.
Otherwise, we can't guarantee anything once the limitation is violated.
In order to manage this serious constraint, the operations that may violate the constraint are marked by the unsafe_ prefix.
The unsafe_inc operation is the dangerous operation.
The unsafe_inc operation simply increments the count state variable with precondition that the value of the variable count is less than 9.
Because calling the unsafe_inc operation with count not less than 9 is prohibited, the inc operation checks if the current state satisfies the precondition of the unsafe_inc operation, and hence the system constraint is secured.
The inc is exported instead of the unsafe_inc operation.
Play in the below sandbox until you get it.
countunsafe_inc()inc()reset()