Skip to content

Commit d8f5eaf

Browse files
committed
Minor Change
1 parent 38e9048 commit d8f5eaf

File tree

2 files changed

+5
-5
lines changed

2 files changed

+5
-5
lines changed

README.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -72,11 +72,11 @@ First of all, let's explore how basic refinements work in LiquidJava.
7272

7373
> Open [RefinementsExample.java](./src/main/java/com/tutorial/part1/RefinementsExample.java)
7474
75-
Here you can find three variables, `positive`, `nonzero` and `percentage`, with comments containing the refinements that should be used in each one. 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.
75+
In the `main` method, you can find four variables, `positive`, `nonzero`, `percentage` and `direction`, with three of them containing comments with the refinements that should be used in each one. 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.
7676

77-
> Now, one by one, uncomment the `@Refinement` annotations and observe each error reported. Remember that only one can be shown at a time. 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`.
77+
> Now, one by one, uncomment the `@Refinement` annotations and observe each error reported. Remember that only one can be shown at a time. 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`.
7878
79-
> Then, try to add a new refinement for a variable `direction`, which ensures its value is always either `-1` or `1` (you should use the `||` operator for this).
79+
> Then, add the refinement for the `direction` variable, which should ensure its value is always either `-1` or `1` (you should use the `||` operator for this). After that, change its value to satisfy the refinement.
8080
8181
As demonstrated previously, we can also refine method parameters and return values.
8282

src/main/java/com/tutorial/part1/RefinementsExample.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ public static void main(String[] args) {
1515
// @Refinement("0 <= _ && _ <= 100")
1616
int percentage = 200;
1717

18-
// add refinement for direction variable here
19-
// ...
18+
// TODO: add refinement to ensure value is either -1 or 1
19+
int direction = 0;
2020
}
2121
}

0 commit comments

Comments
 (0)