Update Docs

Author: rcosta358

pages/annotations/ghosts.md

@@ -39,7 +39,7 @@ s.pop();
 s.pop(); // State Refinement Error
 ```
 
-In the "constructor" method, the ghost variable `size` is initialized to `0`. An equality in a method postcondition is how ghost variables are updated. In this case, the explicit postcondition is optional, because if no postcondition is declared the ghost variable is initialized to its default value, similarly to how Java initializes fields with no explicit initializer (`int -> 0`, `boolean -> false`, and so on).
+In the "constructor" method, the ghost variable `size` is initialized to `0`. An equality in a method postcondition is how ghost variables are updated. If no initial value is declared, the ghost variable is initialized to its default value, similarly to how Java initializes fields with no explicit initializer (`int -> 0`, `boolean -> false`, and so on).
 
 In the `push` method, we specify no precondition, since we can always push an element to the stack, but we specify a postcondition that increments the `size` by one. In this case, we tell the typechecker that the new value of `size` after calling `push` is equal to the old value of `size` plus one. This is possible using the `old` function, which takes an object instance and returns its value before the method call.
 

pages/annotations/state-refinements.md

@@ -56,12 +56,8 @@ public class Buffer {
 }
 ```
 
-If no `to` transition is declared, LiquidJava defaults the constructor to the first state listed in the corresponding `@StateSet`.
-
-Constructors must always be present for typestate checking to work correctly, because they are the point where the initial state values are assigned. Otherwise, the initial values are not set and the verifier won't be able to track the state of the object across method calls.
-
-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.
-
+If no `to` transition is declared, LiquidJava defaults the constructor to the first state of each state set.
+When refining interfaces, which cannot have constructors, a method whose name matches the target class or interface can be used to play the role of a constructor. For example, an interface named `ArrayListRefinements` that is refining the class `java.util.ArrayList` can declare the method `public void ArrayList()` for setting the initial state.
 
 ## Multiple State Sets