Improvements

Author: rcosta358

README.md

@@ -50,17 +50,9 @@ Notice that the method `divide` now requires the parameter `b` to be non-zero. I
 
 To follow along with this tutorial, make sure you have the following prerequisites installed:
 
-- Java 20+, the JDK for compiling and running Java programs
-- Maven 3.6+, for building and dependency management
 - Visual Studio Code, for editing the code and using the LiquidJava extension
 - [Java Extension Pack by Red Hat](vscode:extension/redhat.java), which provides Java support in VS Code
 
-Then, build the project using Maven:
-
-```bash
-mvn clean install
-```
-
 Next, install the [LiquidJava VS Code extension](vscode:extension/AlcidesFonseca.liquid-java). This extension provides the LiquidJava typechecker with real-time error reporting and syntax highlighting for the refinements, which we will use throughout this tutorial.
 
 **Important:** Currently, only one error is reported at a time, so an error might not be reported if another one is present! In each part of the tutorial, make sure to fix all errors before moving on to the next one.
@@ -101,7 +93,7 @@ With this alias, we can replace all occurrences of `@Refinement("_ >= 0")` with
 
 Now, let's explore how to use **state refinements** to specify and verify properties about the state of an object. Open [ExampleStateRefinements.java](./src/main/java/com/tutorial/part2/ExampleStateRefinements.java). Here, we specify that this object can only be in two states: `a` or `b`. Then, in the constructor, we specify that the initial state is `a`, 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.
 
-This object has two methods, also called `a` and `b`. From the state refinements, we can see that the method `a` can only be called when the object is in state `a` transiting to state `b`. Similarly, the method `b` can only be called when the object is in state `b`, transiting to state `a`. 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.
+This object has two methods, `toB` and `toA`. From the state refinements, we can see that the method `toB` can only be called when the object is in state `a` transiting to state `b`. Similarly, the method `toA` can only be called when the object is in state `b`, transiting to state `a`. 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.
 
 #### Exercise
 
@@ -116,7 +108,7 @@ Now, open [ExampleSocketUsage.java](./src/main/java/com/tutorial/part3/ExampleSo
 
 #### Exercise
 
-Now, let's refine another external class. Open [MathRefinements.java](./src/main/java/com/tutorial/part3/exercise/MathRefinements.java). Your task is to replace the `"true"` refinements with the appropriate ones to refine the `java.lang.Math` class. We want to ensure that the `abs` method returns a non-negative value, the `max` method returns the larger of the two arguments, and the `min` method returns the smaller one. To check your implementation, uncomment the code in [MathRefinementsTest.java](./src/main/java/com/tutorial/part3/exercise/MathRefinementsTest.java), which should have no errors after you complete the refinements.
+Now, let's refine another external class. Open [MathRefinements.java](./src/main/java/com/tutorial/part3/exercise/MathRefinements.java). Your task is to replace the `"true"` refinements with the appropriate ones to refine the `java.lang.Math` class. We want to ensure that the `max` method returns the larger of the two arguments and the `min` method returns the smaller one. To check your implementation, uncomment the code in [MathRefinementsTest.java](./src/main/java/com/tutorial/part3/exercise/MathRefinementsTest.java), which should have no errors after you complete the refinements.
 
 ### 4. Ghost Variables
 

src/main/java/com/tutorial/part2/ExampleStateRefinements.java

@@ -10,15 +10,15 @@ public class ExampleStateRefinements {
     public ExampleStateRefinements() {}
 
     @StateRefinement(from="a(this)", to="b(this)")
-    public void a() {}
+    public void toB() {}
 
     @StateRefinement(from="b(this)", to="a(this)")
-    public void b() {}
+    public void toA() {}
 
     public static void main(String[] args) {
         ExampleStateRefinements example = new ExampleStateRefinements();
-        example.a();
-        example.b();
-        // example.b(); // uncomment for error
+        example.toB();
+        example.toA();
+        // example.toA(); // uncomment for error
     }
 }

src/main/java/com/tutorial/part3/exercise/MathRefinements.java

@@ -12,7 +12,7 @@ public interface MathRefinements {
 	@Refinement("_ == 2.7182818284590452354")
 	public double E = 0;
 
-    @Refinement("true")
+    @Refinement("arg0 >= 0 ? _ == arg0 : _ == -arg0")
 	public int abs(int arg0);
 
     @Refinement("true")

src/main/java/com/tutorial/part3/exercise/MathRefinementsTest.java

@@ -11,16 +11,16 @@ public static void test() {
         int a = 2;
         int b = -3;
 
+        @Refinement("_ == 3.141592653589793")
+        double pi = Math.PI;
+        
+        @Refinement("_ == 2.718281828459045")
+        double e = Math.E;
+        
+        @Refinement("_ == 3")
+        int abs = Math.abs(b);
+        
         // // uncomment the lines below after completing MathRefinements.java
-        // @Refinement("_ == 3.141592653589793")
-        // double pi = Math.PI;
-
-        // @Refinement("_ == 2.718281828459045")
-        // double e = Math.E;
-
-        // @Refinement("_ == 3")
-        // int abs = Math.abs(b);
-
         // @Refinement("_ == 2")
         // int max = Math.max(a, b);
 

src/main/java/com/tutorial/part4/ArrayListRefinements.java

@@ -11,8 +11,8 @@ public interface ArrayListRefinements<E> {
 
 	@StateRefinement(to="size(this) == 0")
 	public void ArrayList();
-	
-	@StateRefinement(to="size(this) == (size(old(this)) + 1)")
+
+	@StateRefinement(to="size(this) == size(old(this)) + 1")
 	public boolean add(E elem);
 
 	public E get(@Refinement("0 <= _ && _ < size(this)") int index);

src/main/java/com/tutorial/part4/exercise/StackRefinements.java

@@ -8,6 +8,7 @@
 @Ghost("int count")
 public interface StackRefinements<E> {
 
+	// constructor initializes count to 0 by default
 	public void Stack();
 
 	@StateRefinement(to="true")