Docs: minor fixes

docs/API.md

@@ -26,7 +26,7 @@ Enjoy!
        pre(a > 2 || a == 2); \
        a = a * 2; \
        post(a > 4 || a == 4); \
-     }"
+     }",
   // optional control of which conditions to check
   "options": {"checkPre": true, "checkPost": false}
 }
@@ -49,12 +49,12 @@ The JSON response has the following format:
     <var1>: <value1>
     <var2>: <value2>
     ...
-  }
+  },
   /* in case of non-equivalence, we give all possible truth value-pairs of the specifications */
   "feedback": {
     "pre":  [/*both true*/, /*true, false*/, /*false, true*/, /*both false*/],
     "post": [/*both true*/, /*true, false*/, /*false, true*/, /*both false*/]
-  }
+  },
   "err": /* an error occurred! */
 }
 ```
@@ -83,7 +83,7 @@ There are 3 possible responses:
 ```javascript
 { "responseType": "ResponseErr",
        "err": "(==): heterogeneous types",
-       "model": null.
+       "model": null,
        "feedback": null
 }
 ```

docs/EDSL.md

@@ -39,18 +39,22 @@ We support the standard operations on arithmetic types (`Integer`, `Real`):
 
 ### Polymorphic equality
 
-Any supported type can be compared for equality using the `==` operator, e.g.
+Any supported type can be compared for equality using the `==`/`!=` operator, e.g.
 ```java
 public static void fun(int x, boolean b) {
   pre(x == 1);
   pre(b == true);
   if (x == 1) {
     b = !b;
+    x--;
   }
   post(b == false);
+  post(x != 1);
 }
 ```
 
+There is also a special form for performing null-checking on array **variables**, e.g. `arr != null`
+
 ### Boolean expressions
 
 Every pre/post-condition must be of `Boolean` type.
@@ -58,6 +62,7 @@ Every pre/post-condition must be of `Boolean` type.
 The operations allowed on Booleans are:
  * `&&`: logical conjunction, e.g. `true && false`
  * `||`: logical disjunction, e.g. `true || false`
+ * `!`: logical negation, e.g. `!(true || false)`
  * `imp`: logical implication, e.g. `imp(false, true && false)`
 
 Here is an example specification making use of these operators: