Minor Improvements

Author: rcosta358

pages/concepts/index.md

@@ -4,7 +4,7 @@ nav_order: 2
 has_children: true
 has_toc: false
 permalink: /concepts/
-description: "Browse LiquidJava concepts: for refinements, aliases, state refinements, ghosts, and external refinements."
+description: Learn LiquidJava concepts to understand how to write specifications.
 cards:
   - title: Refinements
     url: /concepts/refinements/

pages/concepts/state-refinements.md

@@ -63,7 +63,7 @@ Constructors must always be present for typestate checking to work correctly, be
 When refining interfaces, which cannot have a constructor, LiquidJava still needs an initialization point. In those cases, the refinement interface must declare a method whose name matches the class we are refining. For example, an interface named `ArrayListRefinements` that is refining `java.util.ArrayList` should declare the method `public void ArrayList()`. This method plays the role of a constructor for the typestate system and ensures the initial values are set correctly.
 
 
-## Multiple StateSets
+## Multiple State Sets
 
 Classes can declare more than one `@StateSet` annotation. This is useful when the object has independent, orthogonal dimensions of state.
 

pages/examples/email.md

@@ -17,46 +17,24 @@ import liquidjava.specification.*;
 
 @StateSet({"empty", "senderSet", "receiverSet", "bodySet"})
 public class Email {
-    private String sender;
-    private List<String> receiver;
-    private String subject;
-    private String body;
 
     @StateRefinement(to="empty()")
-    public Email() {
-        receiver = new ArrayList<>();
-    }
+    public Email() {}
 
     @StateRefinement(from="empty()", to="senderSet()")
-    public void from(String s) {
-        sender = s;
-    }
+    public Email from(String s) {}
 
     @StateRefinement(from="senderSet() || receiverSet()", to="receiverSet()")
-    public void to(String s) {
-        receiver.add(s);
-    }
+    public Email to(String s) {}
 
     @StateRefinement(from="receiverSet()", to="receiverSet()")
-    public void subject(String s) {
-        subject = s;
-    }
+    public Email subject(String s) {}
 
     @StateRefinement(from="receiverSet()", to="bodySet()")
-    public void body(String s) {
-        body = s;
-    }
+    public Email body(String s) {}
 
-    @StateRefinement(from="bodySet()", to="bodySet()")
-    public String build() {
-        StringBuilder sb = new StringBuilder();
-        sb.append("From: " + sender + "\n");
-        sb.append("To: " + String.join(", ", receiver) + "\n");
-        sb.append("Subject: " + subject + "\n");
-        sb.append("\n");
-        sb.append(body);
-        return sb.toString();
-    }
+    @StateRefinement(from="bodySet()")
+    public Email build() {}
 }
 ```
 

pages/examples/order.md

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

pages/getting-started/index.md

@@ -4,7 +4,7 @@ nav_order: 1
 has_children: true
 has_toc: false
 permalink: /getting-started/
-description: Start with the LiquidJava basics, from overview to setup and a first verification run.
+description: Set up your environment and run your first LiquidJava verification.
 cards:
   - title: Setup
     url: /getting-started/setup/

pages/index.md

@@ -8,10 +8,10 @@ description: Documentation for LiquidJava, a lightweight verification system for
 cards:
   - title: Getting Started
     url: /getting-started/
-    description: Learn the basics, set up your environment, and run your first LiquidJava verification.
+    description: Set up your environment and run your first LiquidJava verification.
   - title: Concepts
     url: /concepts/
-    description: Look up LiquidJava concepts, annotations, and protocol rules in a more formal, detailed format.
+    description: Learn LiquidJava concepts to understand how to write specifications.
   - title: Diagnostics
     url: /diagnostics/
     description: Understand LiquidJava errors and warnings.