Rename the UNPROVABLE error category to UNKNOWN

liquidjava-example/src/main/java/testSuite/ErrorUnprovableArgument.java → liquidjava-example/src/main/java/testSuite/ErrorUnknownArgument.java

@@ -2,7 +2,7 @@
 
 import liquidjava.specification.Refinement;
 
-public class ErrorUnprovableArgument {
+public class ErrorUnknownArgument {
 
     static void take(@Refinement("_ > 0") int amount) {}
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java

@@ -10,7 +10,7 @@ public enum ErrorCategory {
     OUT_OF_DOMAIN("A2", "Out of domain: the value is outside what is accepted"),
     ARGUMENT_PICKS_THE_STATE("C3.1", "Argument picks the state: the value passed decides where the object lands"),
     PATH_DEPENDENT_STATE("C4.1", "Path-dependent state: the state differs depending on which branch ran"),
-    UNPROVABLE("C4.2", "Unprovable: nothing is known that could prove the requirement");
+    UNKNOWN("C4.2", "Unknown: nothing is known that could prove the requirement");
 
     private final String id;
     private final String title;

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

@@ -53,11 +53,11 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
                     "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it."));
     }
 
-    /** Unprovable when what was found says nothing about the values the expected refinement constrains */
+    /** Unknown when what was found says nothing about the values the expected refinement constrains */
     private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
         List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
         boolean constrained = expected.getVariableNames().stream().anyMatch(foundVariables::contains);
-        return constrained ? ErrorCategory.OUT_OF_DOMAIN : ErrorCategory.UNPROVABLE;
+        return constrained ? ErrorCategory.OUT_OF_DOMAIN : ErrorCategory.UNKNOWN;
     }
 
     @Override

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java

@@ -60,7 +60,7 @@ public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set
             return List.of();
 
         StateHints hints = new StateHints(machine, receiver);
-        if (category == ErrorCategory.UNPROVABLE)
+        if (category == ErrorCategory.UNKNOWN)
             return hints.reachingCalls(call, goal);
         boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE;
         return Stream.concat(hints.howToReach(current, call, goal, pathDependent).stream(),

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java

@@ -31,7 +31,7 @@ public static Optional<ErrorCategory> categorize(StateMachine machine, Set<State
         List<GhostState> states = ghostStates.stream().filter(g -> g.getParent() != null).toList();
         // all states are possible and none is mentioned: nothing is known, which differs from a join of every state
         if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty())
-            return Optional.of(ErrorCategory.UNPROVABLE);
+            return Optional.of(ErrorCategory.UNKNOWN);
         if (current.size() == 1)
             return Optional.of(ErrorCategory.OUT_OF_ORDER);
         // with several state sets, the states may differ only in a set the call does not check

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java

@@ -50,8 +50,8 @@ void statesDifferingInAnotherStateSetGetNoCategory() {
     }
 
     @Test
-    void unknownStateIsUnprovable() {
-        assertCategory("ErrorStateHintUnknownState.java", ErrorCategory.UNPROVABLE);
+    void nothingKnownAboutStateIsUnknown() {
+        assertCategory("ErrorStateHintUnknownState.java", ErrorCategory.UNKNOWN);
     }
 
     @Test
@@ -70,8 +70,8 @@ void returnValueOutsideItsRefinementIsOutOfDomain() {
     }
 
     @Test
-    void argumentWithNothingKnownIsUnprovable() {
-        assertCategory("ErrorUnprovableArgument.java", ErrorCategory.UNPROVABLE);
+    void argumentWithNothingKnownIsUnknown() {
+        assertCategory("ErrorUnknownArgument.java", ErrorCategory.UNKNOWN);
     }
 
     private static void assertCategory(String test, ErrorCategory expected) {