Add JavaDocs to Classes

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java

@@ -1,5 +1,9 @@
 package liquidjava.diagnostics.errors;
 
+/**
+ * Custom error with an arbitrary message
+ * @see LJError
+ */
 public class CustomError extends LJError {
 
     public CustomError(String message) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java

@@ -3,7 +3,10 @@
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.declaration.CtElement;
 
-// when a ghost call has wrong types or number of arguments
+/**
+ * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments)
+ * @see LJError
+ */
 public class GhostInvocationError extends LJError {
 
     private Predicate expected;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java

@@ -2,7 +2,10 @@
 
 import spoon.reflect.declaration.CtElement;
 
-// when a constructor contains a @StateRefinement with a from state
+/**
+ * Error indicating that a constructor contains a state refinement with a 'from' state, which is not allowed
+ * @see LJError
+ */
 public class IllegalConstructorTransitionError extends LJError {
 
     public IllegalConstructorTransitionError(CtElement element) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java

@@ -2,7 +2,10 @@
 
 import spoon.reflect.declaration.CtElement;
 
-// when a refinement is invalid, e.g. is not a boolean expression
+/**
+ * Error indicating that a refinement is invalid (e.g., not a boolean expression)
+ * @see LJError
+ */
 public class InvalidRefinementError extends LJError {
 
     private String refinement;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java

@@ -5,7 +5,9 @@
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 
-// base class for all LiquidJava errors
+/**
+ * Base class for all LiquidJava errors
+ */
 public abstract class LJError extends Exception {
 
     private String title;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java

@@ -2,7 +2,10 @@
 
 import spoon.reflect.declaration.CtElement;
 
-// e.g. when a variable used in a refinement is not found
+/**
+ * Error indicating that an element referenced in a refinement was not found
+ * @see LJError
+ */
 public class NotFoundError extends LJError {
 
     public NotFoundError(String message, CtElement element) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -5,7 +5,10 @@
 import liquidjava.utils.Utils;
 import spoon.reflect.declaration.CtElement;
 
-// when a @Refinement is violated
+/**
+ * Error indicating that a refinement constraint either was violated or cannot be proven
+ * @see LJError
+ */
 public class RefinementError extends LJError {
 
     private Predicate expected;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java

@@ -3,7 +3,10 @@
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.declaration.CtElement;
 
-// when two incompatible states are found in a state set
+/**
+ * Error indicating that two disjoint states were found in a state refinement
+ * @see LJError
+ */
 public class StateConflictError extends LJError {
 
     private Predicate predicate;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -4,7 +4,10 @@
 
 import spoon.reflect.declaration.CtElement;
 
-// when a @StateRefinement is violated
+/**
+ * Error indicating that a state refinement transition was violated
+ * @see LJError
+ */
 public class StateRefinementError extends LJError {
 
     private final String method;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java

@@ -2,7 +2,10 @@
 
 import spoon.reflect.declaration.CtElement;
 
-// when the syntax of a refinement is invalid
+/**
+ * Error indicating that the syntax of a refinement is invalid
+ * @see LJError
+ */
 public class SyntaxError extends LJError {
 
     private String refinement;