Register Field Contracts Before Forward Declared Writes

liquidjava-example/src/main/java/testSuite/CorrectFieldWriteBeforeTypeDeclaration.java

@@ -0,0 +1,11 @@
+public class CorrectFieldWriteBeforeTypeDeclaration {
+    private final Job job = new Job();
+
+    public void send(int port) {
+        job.port = port;
+    }
+
+    static class Job {
+        int port;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorForwardFieldContract.java

@@ -0,0 +1,14 @@
+import liquidjava.specification.Refinement;
+
+public class ErrorForwardFieldContract {
+    private final Job job = new Job();
+
+    public void send() {
+        job.port = -1; // Expect: Refinement Error
+    }
+
+    static class Job {
+        @Refinement("_ >= 0")
+        int port;
+    }
+}

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

@@ -344,8 +344,13 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
                 ? p : variable.getPosition();
         Predicate cEt;
         RefinedVariable mainRV = null;
-        if (context.hasVariable(simpleName))
+        if (context.hasVariable(simpleName)) {
             mainRV = context.getVariableByName(simpleName);
+        } else {
+            // A field declaration may occur after its first write in the source.
+            // Register its declared contract before attaching the assigned instance.
+            mainRV = context.addVarToContext(simpleName, type, expectedType.orElseGet(Predicate::new), variable);
+        }
 
         if (context.hasVariable(simpleName) && !context.getVariableByName(simpleName).getRefinement().isBooleanTrue()) {
             cEt = mainRV.getMainRefinement();