Fix Comments

Author: rcosta358

pages/concepts/external-refinements.md

@@ -37,6 +37,6 @@ public interface SocketRefinements {
 
 ```java
 Socket socket = new Socket();
-socket.connect(new InetSocketAddress("example.com", 80)); // type error!
+socket.connect(new InetSocketAddress("example.com", 80)); // State Refinement Error
 socket.close();
 ```

pages/concepts/ghosts.md

@@ -35,7 +35,7 @@ public interface StackRefinements<E> {
 Stack<String> s = new Stack<>();
 s.push("hello");
 s.pop();
-s.pop(); // type error!
+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. However, here it is not necessary, since when no postcondition is declared, it is initialized to its default value, similarly to how Java initializes fields to their default values when no explicit initializer is provided (`int --> 0`, `boolean --> false`, etc.). 

pages/concepts/state-refinements.md

@@ -33,7 +33,7 @@ public class File {
 File f = new File();
 f.read();
 f.close();
-f.read(); // type error!
+f.read(); // State Refinement Error
 ```
 
 If a class follows an implicit protocol that can be described by a DFA, the protocol can be encoded in LiquidJava so that methods are enforced to be called in the correct order.

pages/examples/arraylist.md

@@ -29,7 +29,7 @@ public interface ArrayListRefinements<E> {
 ArrayList<Integer> list = new ArrayList<>();
 list.add(1);
 list.get(0);
-list.get(1); // type error!
+list.get(1); // Refinement Error
 ```
 
 The key idea is that LiquidJava turns the usual runtime condition for `get(i)` into a static precondition over the tracked `size` ghost variable.

pages/examples/counter.md

@@ -30,7 +30,7 @@ public class Counter {
 int c = 0;
 c = Counter.increment(c);
 c = Counter.decrement(c);
-c = Counter.decrement(c); // type error!
+c = Counter.decrement(c); // Refinement Error
 ```
 
 The parameter refinement on `decrement` requires the input to be strictly positive, so LiquidJava rejects the final call when `c` is already `0`.

pages/examples/downloader.md

@@ -40,5 +40,5 @@ d.finish();
 Downloader d = new Downloader();
 d.start();
 d.update(50);
-d.finish(); // type error!
-```
+d.finish(); // State Refinement Error
+```

pages/examples/email.md

@@ -74,7 +74,7 @@ email.from("me");
 Email email = new Email();
 email.from("me");
      .to("bob");
-     .build(); // type error!
+     .build(); // State Refinement Error
 ```
 
 LiquidJava enforces the intended protocol:

pages/examples/media-player.md

@@ -38,7 +38,7 @@ player.play();
 player.pause();
 player.resume();
 player.stop();
-player.resume(); // type error!
+player.resume(); // State Refinement Error
 ```
 
 Because `resume` is only valid from `paused()`, the final call is rejected after `stop()` puts the object back in `stopped()`.

pages/examples/order.md

@@ -52,7 +52,7 @@ Order order = new Order();
 order.addItem("shirt", 60)
      .addItem("shoes", 80)
      .checkout()
-     .pay(120); // type error!
+     .pay(120); // State Refinement Error
 ```
 
 This example enforces the intended protocol:

pages/examples/reentrant-lock.md

@@ -31,7 +31,7 @@ public interface ReentrantLockRefinements {
 ReentrantLock lock = new ReentrantLock();
 lock.lock();
 lock.unlock();
-lock.unlock(); // type error
+lock.unlock(); // State Refinement Error
 ```
 
 The external refinement enforces the expected protocol: `lock()` is only allowed when the object is `unlocked()`, and `unlock()` is only allowed when it is `locked()`.