Update Docs

Author: rcosta358

pages/annotations/external-refinements-for.md

@@ -20,16 +20,16 @@ import java.net.*;
 public interface SocketRefinements {
     @StateRefinement(to="unconnected()")
     public void Socket();
-    
+
     @StateRefinement(from="unconnected()", to="bound()")
     public void bind(SocketAddress add);
-    
+
     @StateRefinement(from="bound()", to="connected()")
     public void connect(SocketAddress add);
-    
+
     @StateRefinement(from="connected()")
     public void sendUrgentData(int n);
-    
+
     @StateRefinement(from="!closed()", to="closed()")
     public void close();
 }

pages/annotations/refinement-alias.md

@@ -24,4 +24,4 @@ public class MyClass {
 }
 ```
 
-This helps keep contracts shorter and easier to maintain by giving common constraints a domain-specific name and reusing them in.
+This helps keep contracts shorter and easier to maintain by replacing repeated predicates with a domain-specific alias.

pages/annotations/refinements.md

@@ -43,7 +43,7 @@ Refinement predicates use a language similar to Java, where you can write boolea
 | Logic | `!` `&&` <code>&#124;&#124;</code> `-->` | `@Refinement("0 <= y && y <= 100") int y = 25` |
 | Arithmetic | `+` `-` `*` `/` `%` | `@Refinement("v + 20 < 100") int v = 79` |
 | Conditional | `cond ? e1 : e2` | `@Refinement("a > b ? _ == a : _ == b") int max(int a, int b)` |
-| Ghosts | `ghost(...args)` | `@Refinement("0 <= _ < size(this)") int index` |
+| Ghosts | `ghost(...args)` | `@Refinement("0 <= _ && _ < size(this)") int index` |
 | Aliases | `Alias(...args)` | `@Refinement("Positive(_)") int c = 10` |
 | Literals | `true` `false` `0` `1.5` | `@Refinement("true") void print()` |
 | Enums | `EnumType.Value` | `@Refinement("_ == Status.Open") Status status` |

pages/examples/email.md

@@ -21,20 +21,25 @@ public class Email {
     @StateRefinement(to="empty()")
     public Email() {}
 
+    @Refinement("_ == this")
     @StateRefinement(from="empty()", to="senderSet()")
-    public Email from(String s) {}
+    public Email from(String s) { return this; }
 
+    @Refinement("_ == this")
     @StateRefinement(from="senderSet() || receiverSet()", to="receiverSet()")
-    public Email to(String s) {}
+    public Email to(String s) { return this; }
 
+    @Refinement("_ == this")
     @StateRefinement(from="receiverSet()")
-    public Email subject(String s) {}
+    public Email subject(String s) { return this; }
 
+    @Refinement("_ == this")
     @StateRefinement(from="receiverSet()", to="bodySet()")
-    public Email body(String s) {}
+    public Email body(String s) { return this; }
 
+    @Refinement("_ == this")
     @StateRefinement(from="bodySet()")
-    public Email build() {}
+    public Email build() { return this; }
 }
 ```
 

pages/examples/order.md

@@ -19,14 +19,17 @@ public class Order {
     @StateRefinement(to="ordering() && total() == 0")
     public Order() {}
 
+    @Refinement("_ == this")
     @StateRefinement(from="ordering()", to="ordering() && total() == total(old(this)) + price")
-    public Order addItem(String name, @Refinement("_ > 0") int price) {}
+    public Order addItem(String name, @Refinement("_ > 0") int price) { return this; }
 
+    @Refinement("_ == this")
     @StateRefinement(from="ordering() && total() > 0", to="checkout() && total() == total(old(this))")
-    public Order checkout() {}
+    public Order checkout() { return this; }
 
+    @Refinement("_ == this")
     @StateRefinement(from="checkout() && amount == total()", to="finished()")
-    public Order pay(@Refinement("_ > 0") int amount) {}
+    public Order pay(@Refinement("_ > 0") int amount) { return this; }
 }
 ```
 

pages/getting-started/overview.md

@@ -24,6 +24,8 @@ These make it possible to catch bugs that the standard Java type system cannot,
 ## Example
 
 ```java
+import liquidjava.specification.Refinement;
+
 public class Example {
     public static int divide(int a, @Refinement("b != 0") int b) {
         return a / b;

pages/getting-started/setup.md

@@ -69,4 +69,4 @@ mvn clean install
 
 This runs the verifier on your project and prints any errors to the console.
 
-> You can find more about the command-line interface [here]({{ '/command-line-interface/' | relative_url }}). 
+> You can find more about the command-line interface [here]({{ '/command-line-interface/' | relative_url }}).