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
+76-19Lines changed: 76 additions & 19 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -62,76 +62,133 @@ Currently, **only one error is reported at a time**, so an error might not be re
62
62
63
63
### 1. Basic Refinements
64
64
65
-
First of all, let's explore how basic refinements work in LiquidJava. Open [RefinementsExample.java](./src/main/java/com/tutorial/part1/RefinementsExample.java). Here you can find three variables, `positive`, `nonzero` and `percentage`, with comments containing the refinement that should be used in each one. Remember that only one can be shown at a time. Notice that `_` can also be used as a placeholder for the variable name in the refinement expression, as shown in the refinement for the `percentage` variable.
65
+
First of all, let's explore how basic refinements work in LiquidJava.
66
66
67
-
Now, one by one, uncomment the `@Refinement` annotations and observe each error reported. Then, change each value to satisfy the corresponding refinement — change the value of `positive` to a positive integer, the value of `nonzero` to any non-zero integer, and the value of `percentage` to an integer between `0` and `100`.
67
+
> Open [RefinementsExample.java](./src/main/java/com/tutorial/part1/RefinementsExample.java)
68
68
69
-
As demonstrated previously, we can also refine method parameters and return values. Open [MethodRefinementExample.java](./src/main/java/com/tutorial/part1/MethodRefinementExample.java). Here, the method `divide` is refined to ensure that the parameter `b` is never zero. Try changing the value of the second argument in the `divide` method call to zero and observe the error reported by LiquidJava. Now change it back to a non-zero value.
69
+
Here you can find three variables, `positive`, `nonzero` and `percentage`, with comments containing the refinements that should be used in each one. Remember that only one can be shown at a time. Notice that `_` can also be used as a placeholder for the variable name in the refinement expression, as shown in the refinement for the `percentage` variable.
70
70
71
-
But wait, we can also refine the return value of the method! Let's introduce a bug. Change the implementation of the `divide` method to return `a - b` instead of `a / b`. No error! Let's fix this. Above of the method signature, add the following refinement to specify that the return value should be exactly equal to the division of `a` by `b`:
71
+
> Now, one by one, uncomment the `@Refinement` annotations and observe each error reported. Then, change each value to satisfy the corresponding refinement — change the value of `positive` to a positive integer, the value of `nonzero` to any non-zero integer, and the value of `percentage` to an integer between `0` and `100`.
72
+
73
+
As demonstrated previously, we can also refine method parameters and return values.
74
+
75
+
> Open [MethodRefinementExample.java](./src/main/java/com/tutorial/part1/MethodRefinementExample.java).
76
+
77
+
Here, the method `divide` is refined to ensure that the parameter `b` is never zero.
78
+
79
+
> Try changing the value of the second argument in the `divide` method call to zero and observe the error reported by LiquidJava. Now change it back to a non-zero value.
80
+
81
+
But wait, we can also refine the return value of the method! Let's introduce a bug.
82
+
83
+
> Change the implementation of the `divide` method to return `a - b` instead of `a / b`.
84
+
85
+
No error! Let's fix this.
86
+
87
+
> Above of the method signature, add the following refinement to specify that the return value should be exactly equal to the division of `a` by `b`:
72
88
73
89
```java
74
90
@Refinement("_ == a / b")
75
91
```
76
92
77
-
Now we get an error! LiquidJava is telling us that the implementation of the method does not satisfy the refinement specified for the return value. This way, we can catch errors not only in the inputs of the methods, but also in their outputs. Fix the implementation of the method to return `a / b` again to make the error disappear.
93
+
Now we get an error! LiquidJava is telling us that the implementation of the method does not satisfy the refinement specified for the return value. This way, we can catch errors not only in the inputs of the methods, but also in their outputs.
94
+
95
+
> Fix the implementation of the method to return `a / b` again to make the error disappear.
78
96
79
97
#### Exercise
80
98
81
-
Now, open [Bank.java](./src/main/java/com/tutorial/part1/exercise/Bank.java). This class simulates a simple bank account with two methods: `deposit` and `withdraw`. Now, open [BankExample.java](./src/main/java/com/tutorial/part1/exercise/BankExample.java). Here we simulate a wrong usage of the `deposit` and `withdraw` methods of a bank account, since it tries to withdraw more money than the current balance. Let's make use of LiquidJava refinements to ensure the correct usage of these methods. In `Bank.java`, replace the `"true"` refinements with the appropriate ones to ensure the correct behavior of both methods. For example, we want to ensure that the `balance` and `amount` parameters of both methods are equal or greater than zero and greater than zero, respectively. Also, we want to ensure the correct implementation of both methods — they must return the updated balance after the deposit or withdrawal operations. This also tells the typechecker what the expected output is, allowing it to verify the correctness of the following operations.
99
+
> Open [Bank.java](./src/main/java/com/tutorial/part1/exercise/Bank.java).
100
+
101
+
This class simulates a simple bank account with two methods: `deposit` and `withdraw`. In the `main` method, we simulate a wrong usage of the `deposit` and `withdraw` methods of a bank account, since it tries to withdraw more money than the current balance. Let's make use of LiquidJava refinements to ensure the correct usage of these methods.
102
+
103
+
> Replace the `"true"` refinements with the appropriate ones to ensure the correct behavior of both methods.
104
+
105
+
For example, we want to ensure that the `balance` and `amount` parameters of both methods are equal or greater than zero and greater than zero, respectively. Also, we want to ensure the correct implementation of both methods — they must return the updated balance after the deposit or withdrawal operations. This also tells the typechecker what the expected output is, allowing it to verify the correctness of the following operations.
82
106
83
107
With the correct refinements in place, LiquidJava will report an error in the `withdraw` method call, since it tries to withdraw more money than it was deposited. If we instead try to withdraw `10` or less, no error will be reported.
84
108
85
-
However, notice that we are repeating the same refinement twice in the `balance` parameter of both methods. For this, we can use a refinement aliases to define commonly used refinements and avoid repetition. Add the following lines of code above the class definition:
109
+
However, notice that we are repeating the same refinement twice in the `balance` parameter of both methods. For this, we can use a refinement aliases to define commonly used refinements and avoid repetition.
110
+
111
+
> Add the following lines of code above the class definition:
86
112
87
113
```java
88
114
importliquidjava.specification.RefinementAlias;
89
115
90
116
@RefinementAlias("NonNegative(int v) { v >= 0 }")
91
117
```
92
118
93
-
With this alias, we can replace all occurrences of `@Refinement("_ >= 0")` with `@Refinement("NonNegative(_)")`, and it will achieve the same effect!
119
+
> Then, replace all occurrences of `@Refinement("_ >= 0")` with `@Refinement("NonNegative(_)")`.
120
+
121
+
The refinements are now easier to understand, while still providing the same guarantees!
94
122
95
123
### 2. State Refinements
96
124
97
-
Now, let's explore how to use **state refinements** to specify and verify properties about the state of an object. Open [LightBulb.java](./src/main/java/com/tutorial/part2/LightBulb.java). Here, we specify that this object can only be in two states: `on` or `off`. Then, in the constructor, we specify that the initial state is `off`, through the `@StateRefinement` annotation. This annotation allows us to specify in which state the object should be before the method is called (`from`), and in which state it will be after the method execution (`to`). In the constructor, since it's the first method to be called, we can only specify the `to` state.
125
+
Let's explore how to use **state refinements** to specify and verify properties about the state of an object.
126
+
127
+
> Open [LightBulb.java](./src/main/java/com/tutorial/part2/LightBulb.java).
98
128
99
-
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. Try uncommenting line 22 to observe the error.
129
+
Here, we specify that this object can only be in two states: `on` or `off`. Then, in the constructor, we specify that the initial state is `off`, through the `@StateRefinement` annotation. This annotation allows us to specify in which state the object should be before the method is called (`from`), and in which state it will be after the method execution (`to`). In the constructor, since it's the first method to be called, we can only specify the `to` state.
130
+
131
+
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.
132
+
133
+
> Uncomment line 22 to observe the error and then comment it back again.
100
134
101
135
#### Exercise
102
136
103
-
Open [MediaPlayer.java](./src/main/java/com/tutorial/part2/exercise/MediaPlayer.java). Your task is to replace the `"true"` refinements with the appropriate ones to ensure the correct behavior of the `play`, `pause`, `resume` and `stop` methods, using the `stopped`, `playing`, and `paused` states. 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 use the `!` operator for this).
137
+
> Open [MediaPlayer.java](./src/main/java/com/tutorial/part2/exercise/MediaPlayer.java). Your task is to replace the `"true"` refinements with the appropriate ones to ensure the correct behavior of the `play`, `pause`, `resume` and `stop` methods, using the `stopped`, `playing`, and `paused` states.
104
138
105
-
With the correct implementation, LiquidJava will report an error in line 10 of [MediaPlayerExample.java](./src/main/java/com/tutorial/part2/exercise/MediaPlayerExample.java), since we are trying to resume playback when the player is stopped.
139
+
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 use the `!` operator for this).
140
+
141
+
With the correct implementation, LiquidJava will report an error in line 30, since we are trying to resume playback when the player is stopped.
106
142
107
143
### 3. External Refinements
108
144
109
-
To demonstrate the state refinements in a real world scenario, let's learn about **external refinements**. LiquidJava allows us to refine external classes, such as classes from the Java standard library. For instance, we can refine the `Socket` class to ensure its correct usage. Open [SocketRefinements.java](./src/main/java/com/tutorial/part3/SocketRefinements.java). 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.
145
+
To demonstrate the state refinements in a real world scenario, let's learn about **external refinements**. LiquidJava allows us to refine external classes, such as classes from the Java standard library. For instance, we can refine the `Socket` class to ensure its correct usage.
146
+
147
+
> Open [SocketRefinements.java](./src/main/java/com/tutorial/part3/SocketRefinements.java).
110
148
111
-
Now, open [SocketExample.java](./src/main/java/com/tutorial/part3/SocketExample.java). Here, we see a simple usage of the `Socket` class. If you comment out the line 9 containing with the `bind` method call, LiquidJava will report an error in the `connect` method call, since it violates the state refinement specified for the `Socket` class! Notice that when using the `Socket` class, we don't need to deal with any refinement annotations, since they are already specified in the external refinement interface.
149
+
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.
150
+
151
+
> Open [SocketExample.java](./src/main/java/com/tutorial/part3/SocketExample.java).
152
+
153
+
Here, we see a simple usage of the `Socket` class. If you comment out the line 9 containing with the `bind` method call, LiquidJava will report an error in the `connect` method call, since it violates the state refinement specified for the `Socket` class! Notice that when using the `Socket` class, we don't need to deal with any refinement annotations, since they are already specified in the external refinement interface.
112
154
113
155
114
156
#### Exercise
115
157
116
-
Now, let's refine another external class. Open [ReentrantLockRefinements.java](./src/main/java/com/tutorial/part3/exercise/ReentrantLockRefinements.java). Your task is to replace the `"true"` refinements with the appropriate ones to refine the `ReentrantLock` class. 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.
158
+
Let's refine another external class.
159
+
160
+
> Open [ReentrantLockRefinements.java](./src/main/java/com/tutorial/part3/exercise/ReentrantLockRefinements.java). Your task is to replace the `"true"` refinements with the appropriate ones to refine the `ReentrantLock` class.
117
161
118
-
With the correct implementation, LiquidJava will report an error in line 11 of [ReentrantLockExample.java](./src/main/java/com/tutorial/part3/exercise/ReentrantLockExample.java), since we are trying to unlock a lock that is not locked.
162
+
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.
163
+
164
+
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.
119
165
120
166
121
167
### 4. Ghost Variables
122
168
123
-
Finally, LiquidJava also offers a way to model objects using **ghost variables** through the `@Ghost` annotation, which are used to track additional information about the program's state when states aren't enough. These can be, for instance, counters (integers) or flags (booleans), to model more complex protocols. To demonstrate this, open [ArrayListRefinements.java](./src/main/java/com/tutorial/part4/ArrayListRefinements.java). Here, we define the refinements for the `ArrayList` class, using a ghost variable `size` to keep track of the number of elements in the list. Using the `size` ghost variable in state refinements, we can prevent out-of-bounds access.
169
+
Finally, LiquidJava also offers a way to model objects using **ghost variables** through the `@Ghost` annotation, which are used to track additional information about the program's state when states aren't enough. These can be, for instance, counters (integers) or flags (booleans), to model more complex protocols.
170
+
171
+
> Open [ArrayListRefinements.java](./src/main/java/com/tutorial/part4/ArrayListRefinements.java).
172
+
173
+
Here, we define the refinements for the `ArrayList` class, using a ghost variable `size` to keep track of the number of elements in the list. Using the `size` ghost variable in state refinements, we can prevent out-of-bounds access.
124
174
125
175
In the constructor, we specify that after it is called, the ghost variable `size` will be equal to `0`. This is optional since its default value is already zero, but it helps us understand this example. Then, in the `add` method, we specify that it can be called in any state (since we don't specify a `from` state), and that after it is called, the `size` ghost variable will be incremented by one — the new size will be equal to the old size plus one (`old` is a special keyword that refers to the previous state of the object, so calling `size(old(this))` gets the value of `size` before the method was called). Finally, in the `get` method, we specify that the index parameter must be non-negative and less than the current size of the list, therefore preventing out-of-bounds errors.
126
176
127
-
In [ArrayListExample.java](./src/main/java/com/tutorial/part4/ArrayListExample.java), we can see a simple usage of the refined `ArrayList` class. If you uncomment line 11, LiquidJava will report an error, since we are trying to access an index that is out of bounds!
177
+
> Open [ArrayListExample.java](./src/main/java/com/tutorial/part4/ArrayListExample.java).
178
+
179
+
Here, we can see a simple usage of the refined `ArrayList` class. If you uncomment line 11, LiquidJava will report an error, since we are trying to access an index that is out of bounds!
128
180
129
181
#### Exercise
130
182
131
-
Now, let's try to do the same but for the `Stack` class. Open [StackRefinements.java](./src/main/java/com/tutorial/part4/exercise/StackRefinements.java). Your task is to refine the `Stack` class by replacing the `"true"` refinements with the appropriate ones to ensure the correct behavior of the `push`, `pop` and `peek` methods, using the `count` ghost variable to keep track of the number of elements in the stack, and not allow incorrect uses of these methods — popping or peeking from an empty stack. With the correct implementation, LiquidJava will report an error in line 11 of [StackExample.java](./src/main/java/com/tutorial/part4/exercise/StackExample.java), since we are trying to pop an element of the stack when it is empty.
183
+
Let's do the same but for the `Stack` class.
184
+
185
+
> Open [StackRefinements.java](./src/main/java/com/tutorial/part4/exercise/StackRefinements.java). Your task is to refine the `Stack` class by replacing the `"true"` refinements with the appropriate ones to ensure the correct behavior of the `push`, `pop` and `peek` methods, using the `count` ghost variable to keep track of the number of elements in the stack, and not allow incorrect uses of these methods — popping or peeking from an empty stack.
186
+
187
+
With the correct implementation, LiquidJava will report an error in line 11 of [StackExample.java](./src/main/java/com/tutorial/part4/exercise/StackExample.java), since we are trying to pop an element of the stack when it is empty.
0 commit comments