Improve Method Names & Javadocs

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -16,7 +16,6 @@
 import liquidjava.processor.facade.GhostDTO;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.RefinementsParser;
-import liquidjava.smt.Counterexample;
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
@@ -315,7 +314,8 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen
     }
 
     public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
-        SMTResult result = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
+        SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostState(), p,
+                factory);
         return result.isOk();
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -56,43 +56,41 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
             e.setPosition(element.getPosition());
             throw e;
         }
-        SMTResult result = smtChecks(expected, premises, element.getPosition());
+        SMTResult result = verifySMTSubtype(expected, premises, element.getPosition());
         if (result.isError()) {
             throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
                     map, result.getCounterexample(), customMessage);
         }
     }
 
     /**
-     * Check that type is a subtype of expectedType Throws RefinementError otherwise
-     *
+     * Checks if type is a subtype of expectedType
+     * 
      * @param type
      * @param expectedType
      * @param list
      * @param element
      * @param f
-     *
+     * 
      * @throws LJError
      */
     public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
             Factory f) throws LJError {
-        SMTResult result = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
+        SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
         if (result.isError())
             throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null);
     }
 
     /**
-     * Checks the expected against the found constraint
-     *
+     * Verifies whether the found predicate is a subtype of the expected predicate
+     * 
      * @param expected
      * @param found
      * @param position
-     *
-     * @return counterexample if expected type is not subtype of found type, otherwise null
-     *
-     * @throws LJError
+     * 
+     * @return the result of the verification, containing a counterexample if the verification fails
      */
-    public SMTResult smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
+    public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePosition position) throws LJError {
         try {
             return new SMTEvaluator().verifySubtype(found, expected, context);
         } catch (LJError e) {
@@ -103,8 +101,19 @@ public SMTResult smtChecks(Predicate expected, Predicate found, SourcePosition p
         }
     }
 
-    public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
-            SourcePosition position, Factory f) throws LJError {
+    /**
+     * Verifies whether the found predicate is a subtype of the expected predicate, taking into account the ghost states
+     * 
+     * @param type
+     * @param expectedType
+     * @param states
+     * @param position
+     * @param factory
+     * 
+     * @return the result of the verification, containing a counterexample if the verification fails
+     */
+    public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List<GhostState> states,
+            SourcePosition position, Factory factory) throws LJError {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
         gatherVariables(type, lrv, mainVars);
@@ -114,13 +123,14 @@ public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, Lis
         TranslationTable map = new TranslationTable();
         String[] s = { Keys.WILDCARD, Keys.THIS };
         Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
-        List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
+        List<GhostState> filtered = filterGhostStatesForVariables(states, mainVars, lrv);
         premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s)
-                .changeAliasToRefinement(context, f);
-        Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
+                .changeAliasToRefinement(context, factory);
+        Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context,
+                factory);
 
         // check subtyping
-        return smtChecks(expected, premises, position);
+        return verifySMTSubtype(expected, premises, position);
     }
 
     /**

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -13,26 +13,36 @@
 
 public class SMTEvaluator {
 
-    public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception {
-        // Creates a parser for our SMT-ready refinement language
-        // Discharges the verification to z3
+    /**
+     * Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser
+     * for our SMT-ready refinement language and discharges the verification to Z3
+     * 
+     * @param subRef
+     * @param supRef
+     * @param context
+     * 
+     * @return the result of the verification, containing a counterexample if the verification fails
+     */
+    public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception {
         Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
         try {
             Expression exp = toVerify.getExpression();
-            try (TranslatorToZ3 tz3 = new TranslatorToZ3(c)) {
+            try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
                 ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
                 Expr<?> e = exp.accept(visitor);
                 Solver solver = tz3.makeSolverForExpression(e);
                 Status result = solver.check();
+
+                // subRef is not a subtype of supRef
                 if (result.equals(Status.SATISFIABLE)) {
                     Model model = solver.getModel();
                     Counterexample counterexample = tz3.getCounterexample(model);
                     return SMTResult.error(counterexample);
                 }
             }
-        } catch (SyntaxException e1) {
+        } catch (SyntaxException e) {
             System.out.println("Could not parse: " + toVerify);
-            e1.printStackTrace();
+            e.printStackTrace();
         } catch (Z3Exception e) {
             throw new Z3Exception(e.getLocalizedMessage());
         }