You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+7-5Lines changed: 7 additions & 5 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -144,7 +144,7 @@ Here, we specify that this object can only be in two states: `on` or `off`. Then
144
144
145
145
This object has two methods, `turnOn` and `turnOff`. From the state refinements, we can see that the method `turnOn` can only be called when the object is in state `off` transiting to state `on`. Similarly, the method `turnOff` can only be called when the object is in state `on`, transiting to state `off`. This means that we cannot call the same method twice in a row, since it would violate the protocol established by the state refinements. The following DFA illustrates this:
> Uncomment line 22 to observe the error and then comment it back again.
150
150
@@ -154,7 +154,7 @@ This object has two methods, `turnOn` and `turnOff`. From the state refinements,
154
154
155
155
For example, we want to ensure that the `pause` method can only be called when the player is playing, and that the `stop` method can only be called when the player is not stopped (you can either use the `!` or the `||` operator for this). The state transitions are represented by the following DFA:
156
156
157
-
157
+
158
158
159
159
If you get stuck, here are some **hints**:
160
160
@@ -173,7 +173,7 @@ To demonstrate the state refinements in a real world scenario, let's learn about
173
173
174
174
Here, we refine the `Socket` class through state refinements, with the possible states being `unconnected`, `bound`, `connected`, and `closed`. Then, for each method, we specify the allowed state transitions. This way, we can ensure that, for example, the `connect` method can only be called after the `bind` method, and that the `close` method can only be called once. The following DFA details the allowed state transitions:
175
175
176
-
176
+
177
177
178
178
> Open [SocketExample.java](./src/main/java/com/tutorial/part3/SocketExample.java).
179
179
@@ -187,7 +187,7 @@ Let's refine another external class.
187
187
188
188
We want to ensure that the `lock` method can only be called in the `unlocked` state, and that the `unlock` method can only be called in the `locked` state. These transitions are represented by the following DFA:
With the correct implementation, LiquidJava will report an error in line 10 of [ReentrantLockExample.java](./src/main/java/com/tutorial/part3/exercise/ReentrantLockExample.java), since we are trying to unlock a lock that is not locked. Remember to fix the error before moving on.
193
193
@@ -224,7 +224,9 @@ With the correct implementation, LiquidJava will report an error in line 11 of [
224
224
225
225
> Open [Downloader.java](./src/main/java/com/tutorial/part5/Downloader.java). Your task is to refine the `Downloader` class by replacing the `"true"` refinements with the appropriate ones to ensure the correct behavior of the `start`, `updateProgress`, `complete` and `getFile` methods, using the `progress` ghost variable to keep track of the download progress (from `0` to `100`), and not allow incorrect uses of these methods.
226
226
227
-
You will have to use most of the concepts learned throughout this tutorial, including refinement aliases, state refinements, and ghost variables.
227
+
You will have to use most of the concepts learned throughout this tutorial, including refinement aliases, state refinements, and ghost variables. The following DFA illustrates the allowed state transitions:
0 commit comments