Add Challenge

Author: rcosta358

README.md

@@ -220,6 +220,21 @@ If you get stuck, here are some **hints**:
 
 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.
 
+### 5. Challenge
+
+> 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.
+
+You will have to use most of the concepts learned throughout this tutorial, including refinement aliases, state refinements, and ghost variables.
+
+If you get stuck, here are some **hints**:
+
+- The refinement alias `Percent` should only allow integers between `0` and `100` and then it should be used to refine the `percentage` parameter of the `updateProgress` method
+- You should combine states and ghost variable assertions in the state refinements of the `updateProgress` and `complete` methods using the `&&` operator
+- You should define that the new percentage value in the `updateProgress` method should always be greater than the current `progress` ghost variable value
+- The `getFile` method should only be called when the download is finished
+
+With the correct implementation, LiquidJava should report an error in line 35, since we are trying to complete the download when the progress is not yet `100%`. Simply add a new line that updates the progress to `100` before calling the `complete` method to fix the error.
+
 ---
 
 ## Quiz

src/main/java/com/tutorial/part5/Downloader.java

@@ -0,0 +1,39 @@
+package com.tutorial.part5;
+
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateSet;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.Refinement;
+
+@RefinementAlias("Percent(int x) { true }")
+@StateSet({"waiting", "downloading", "finished"})
+@Ghost("int progress")
+public class Downloader {
+
+    @StateRefinement(to="waiting(this)")
+    public Downloader() {}
+
+    @StateRefinement(from="true", to="true")
+    public void start() {}
+
+    @StateRefinement(from="true", to="true")
+    @Refinement("true")
+    public void updateProgress(@Refinement("true") int percentage) {}
+
+    @StateRefinement(from="true", to="true")
+    public void complete() {}
+
+    @StateRefinement(from="true")
+    public void getFile() {}
+
+    public static void main(String[] args) {
+        Downloader d = new Downloader();
+        d.start();
+        d.updateProgress(30);
+        d.updateProgress(70);
+        d.complete(); // should be an error
+        d.getFile();
+    }
+}
+