Corrections

Author: rcosta358

pages/annotations/refinement-predicates.md

@@ -18,9 +18,7 @@ The `@Ghost` and `@StateSet` annotations are sugar for the `@RefinementPredicate
 | `@Ghost("boolean open")` | `@RefinementPredicate("boolean open(InputStreamReader)")` |
 | `@StateSet({"open", "closed"})` | `@RefinementPredicate("int state1(File)")`<br>`state1(this) == 0 <=> open(this)`<br>`state1(this) == 1 <=> closed(this)` |
 
-In the current implementation, `@RefinementPredicate` is only supported on methods and constructors, but it is not currently scoped to the annotated method or constructor. Instead, is a global declaration that is available for the whole verification.
-
-## What's a Ghost Function?
+## Ghost Functions
 
 A ghost function is an uninterpreted function used only during verification. In practice, that means:
 
@@ -51,7 +49,7 @@ The meaning comes from those constraints, not from a body.
 
 ## Example
 
-You can model any typestate protocol without using the `@StateSet` annotation, by declaring a ghost function that represents the state and then using aliases to give names to the different states, which is kind of like how `@StateSet` works. Under the hood, states are just ghost functions that return an integer representing current the state. For example:
+You can model any typestate protocol without using the `@StateSet` annotation, by declaring a ghost function that represents the state and then using aliases to give names to the different states, which is kind of like how `@StateSet` works. Under the hood, states are just ghost functions that return an integer representing the current state. For example:
 
 ```java
 import liquidjava.specification.*;

pages/examples/downloader.md

@@ -13,6 +13,7 @@ This example models a simple downloader object that tracks the progress of a dow
 ```java
 import liquidjava.specification.*;
 
+@RefinementAlias("Percentage(int p) { 0 <= p && p <= 100 }")
 @Ghost("int progress")
 @StateSet({"created", "downloading", "completed"})
 public class Downloader {
@@ -22,8 +23,8 @@ public class Downloader {
     @StateRefinement(from="created() && progress() == 0", to="downloading() && progress() == 0")
     public void start() {}
 
-    @StateRefinement(from="downloading()", to="downloading() && progress() == percentage")
-    public void update(@Refinement("percentage > progress()") int percentage) {}
+    @StateRefinement(from="downloading() && percentage > progress()", to="downloading() && progress() == percentage")
+    public void update(@Refinement("Percentage(_)") int percentage) {}
 
     @StateRefinement(from="downloading() && progress() == 100", to="completed()")
     public void finish() {}

pages/examples/email.md

@@ -27,7 +27,7 @@ public class Email {
     @StateRefinement(from="senderSet() || receiverSet()", to="receiverSet()")
     public Email to(String s) {}
 
-    @StateRefinement(from="receiverSet()", to="receiverSet()")
+    @StateRefinement(from="receiverSet()")
     public Email subject(String s) {}
 
     @StateRefinement(from="receiverSet()", to="bodySet()")
@@ -59,5 +59,5 @@ LiquidJava enforces the intended protocol:
 
 - The `from` must be set first
 - The `to` must be set at least once before setting the `body`
-- The `subject` is optional
+- The `subject` is optional, but if used it must be set before the `body`
 - The `build` method can only be called after the body is set