Derive Developer Facing States

liquidjava-example/src/main/java/testSuite/classes/imagewrite_correct/ImageWriteParamsRefinements.java

@@ -0,0 +1,88 @@
+package testSuite.classes.imagewrite_correct;
+
+import java.util.Locale;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * External typestate specification for {@code javax.imageio.ImageWriteParam}.
+ *
+ * <p>
+ * The class is modelled as two independent ghost-state dimensions — tiling and compression — so a configuration error
+ * in one dimension does not mask the other. The conditional {@code setTilingMode} / {@code setCompressionMode}
+ * transitions only reach the {@code *Explicit} state when called with {@code MODE_EXPLICIT}; any other mode leaves the
+ * param in its {@code start*} state, which the dimension-specific setters reject.
+ */
+@StateSet({ "startTiling", "tilingExplicit", "tilingSet" })
+@StateSet({ "startCompression", "compressionExplicit", "compressionSet" })
+@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
+public interface ImageWriteParamsRefinements {
+
+    // Constructor
+    @StateRefinement(to = "startTiling(this) && startCompression(this)")
+    void ImageWriteParam(Locale locale);
+
+    // Tiling related methods
+
+    @StateRefinement(to = "(mode == ImageWriteParam.MODE_EXPLICIT)? tilingExplicit(this) : startTiling(this)")
+    void setTilingMode(int mode);
+
+    @StateRefinement(from = "tilingExplicit(this)", to = "tilingSet(this)")
+    @StateRefinement(from = "tilingSet(this)", to = "tilingSet(this)")
+    void setTiling(@Refinement("_ > 0") int tileWidth, @Refinement("_ > 0") int tileHeight, int tileGridXOffset,
+            int tileGridYOffset);
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileGridXOffset();
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileGridYOffset();
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileHeight();
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileWidth();
+
+    @StateRefinement(from = "tilingExplicit(this)")
+    @StateRefinement(from = "tilingSet(this)", to = "tilingExplicit(this)")
+    void unsetTiling();
+
+    void setProgressiveMode(@Refinement("ImageWriteParam.MODE_DISABLED == mode || mode == ImageWriteParam.MODE_DEFAULT || mode == ImageWriteParam.MODE_COPY_FROM_METADATA") int mode);
+
+    // Compression related methods
+
+    @StateRefinement(to = "mode == ImageWriteParam.MODE_EXPLICIT? compressionExplicit(this) : startCompression(this)")
+    void setCompressionMode(int mode);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    void setCompressionQuality(@Refinement("_ >= 0.0 && _ <= 1.0") float quality);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    String getCompressionType();
+
+    @StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)")
+    void setCompressionType(String compressionType);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)", to = "compressionExplicit(this)")
+    void unsetCompression();
+
+    @StateRefinement(from = "compressionSet(this)")
+    String getLocalizedCompressionTypeName();
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    boolean isCompressionLossless();
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    float getCompressionQuality();
+}

liquidjava-example/src/main/java/testSuite/classes/imagewrite_correct/JpegExporter.java

@@ -0,0 +1,32 @@
+package testSuite.classes.imagewrite_correct;
+
+import java.util.Locale;
+
+import javax.imageio.ImageWriteParam;
+
+/**
+ * A JPEG export pipeline configured correctly against {@link ImageWriteParamsRefinements}.
+ *
+ * <p>
+ * Both ghost-state dimensions are driven through their full transition path: each dimension's mode is set to
+ * {@code MODE_EXPLICIT} before the dimension-specific setters run, and {@code getTileWidth} is reached only after
+ * {@code setTiling} has moved the param into {@code tilingSet}. No state refinement is violated.
+ */
+class JpegExporter {
+
+    ImageWriteParam buildJpegParam() {
+        ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
+        param.setTilingMode(ImageWriteParam.MODE_EXPLICIT);
+        param.setTiling(10, 30, 10, 30);
+        param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
+        param.setCompressionQuality(0.85f);
+        return param;
+    }
+
+    int firstTileWidth() {
+        ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
+        param.setTilingMode(ImageWriteParam.MODE_EXPLICIT);
+        param.setTiling(8, 8, 0, 0);
+        return param.getTileWidth();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/imagewrite_error/ImageWriteParamsRefinements.java

@@ -0,0 +1,88 @@
+package testSuite.classes.imagewrite_error;
+
+import java.util.Locale;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * External typestate specification for {@code javax.imageio.ImageWriteParam}.
+ *
+ * <p>
+ * The class is modelled as two independent ghost-state dimensions — tiling and compression — so a configuration error
+ * in one dimension does not mask the other. The conditional {@code setTilingMode} / {@code setCompressionMode}
+ * transitions only reach the {@code *Explicit} state when called with {@code MODE_EXPLICIT}; any other mode leaves the
+ * param in its {@code start*} state, which the dimension-specific setters reject.
+ */
+@StateSet({ "startTiling", "tilingExplicit", "tilingSet" })
+@StateSet({ "startCompression", "compressionExplicit", "compressionSet" })
+@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
+public interface ImageWriteParamsRefinements {
+
+    // Constructor
+    @StateRefinement(to = "startTiling(this) && startCompression(this)")
+    void ImageWriteParam(Locale locale);
+
+    // Tiling related methods
+
+    @StateRefinement(to = "(mode == ImageWriteParam.MODE_EXPLICIT)? tilingExplicit(this) : startTiling(this)")
+    void setTilingMode(int mode);
+
+    @StateRefinement(from = "tilingExplicit(this)", to = "tilingSet(this)")
+    @StateRefinement(from = "tilingSet(this)", to = "tilingSet(this)")
+    void setTiling(@Refinement("_ > 0") int tileWidth, @Refinement("_ > 0") int tileHeight, int tileGridXOffset,
+            int tileGridYOffset);
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileGridXOffset();
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileGridYOffset();
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileHeight();
+
+    @StateRefinement(from = "tilingSet(this)")
+    int getTileWidth();
+
+    @StateRefinement(from = "tilingExplicit(this)")
+    @StateRefinement(from = "tilingSet(this)", to = "tilingExplicit(this)")
+    void unsetTiling();
+
+    void setProgressiveMode(@Refinement("ImageWriteParam.MODE_DISABLED == mode || mode == ImageWriteParam.MODE_DEFAULT || mode == ImageWriteParam.MODE_COPY_FROM_METADATA") int mode);
+
+    // Compression related methods
+
+    @StateRefinement(to = "mode == ImageWriteParam.MODE_EXPLICIT? compressionExplicit(this) : startCompression(this)")
+    void setCompressionMode(int mode);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    void setCompressionQuality(@Refinement("_ >= 0.0 && _ <= 1.0") float quality);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    String getCompressionType();
+
+    @StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)")
+    void setCompressionType(String compressionType);
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)", to = "compressionExplicit(this)")
+    void unsetCompression();
+
+    @StateRefinement(from = "compressionSet(this)")
+    String getLocalizedCompressionTypeName();
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    boolean isCompressionLossless();
+
+    @StateRefinement(from = "compressionExplicit(this)")
+    @StateRefinement(from = "compressionSet(this)")
+    float getCompressionQuality();
+}

liquidjava-example/src/main/java/testSuite/classes/imagewrite_error/JpegExporter.java

@@ -0,0 +1,29 @@
+package testSuite.classes.imagewrite_error;
+
+import java.util.Locale;
+
+import javax.imageio.ImageWriteParam;
+
+/**
+ * A JPEG export pipeline configured against {@link ImageWriteParamsRefinements}.
+ *
+ * <p>
+ * The author did configure a tiling mode — but passed {@code MODE_DEFAULT} instead of {@code MODE_EXPLICIT}. The spec's
+ * conditional transition leaves the param in {@code startTiling} for any non-explicit mode, so {@code setTiling}
+ * (which requires {@code tilingExplicit} or {@code tilingSet}) violates its from-state.
+ *
+ * <p>
+ * The found-state threads the same {@code param} across SSA versions joined by internal {@code stateN(x) == stateN(y)}
+ * equalities; state derivation rewrites those into developer-facing typestate names for the diagnostic.
+ */
+class JpegExporter {
+
+    ImageWriteParam buildJpegParam() {
+        ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
+        param.setTilingMode(ImageWriteParam.MODE_DEFAULT);
+        param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
+        param.setCompressionQuality(0.85f);
+        param.setTiling(10, 30, 10, 30); // State Refinement Error
+        return param;
+    }
+}

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

@@ -391,6 +391,9 @@ protected void throwStateRefinementError(SourcePosition position, Predicate foun
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
+        // simplify(context) folds the found-state predicate and, in the same pass, rewrites internal
+        // ghost-state equalities into developer-facing state predicates (see ExpressionSimplifier /
+        // StateDerivation). The resulting ValDerivationNode keeps the provenance of that rewrite.
         throw new StateRefinementError(position, expected.simplify(context),
                 foundState.toConjunctions().simplify(context), map, customMessage);
     }

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -257,8 +257,9 @@ public ValDerivationNode simplify(Context context) {
         for (AliasWrapper aw : context.getAliases()) {
             aliases.put(aw.getName(), aw.createAliasDTO());
         }
-        // simplify expression
-        ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases);
+        // simplify expression — ghost states let the simplifier rewrite internal state equalities into
+        // developer-facing state predicates for error messages
+        ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases, context.getGhostStates());
         DebugLog.simplification(this.getExpression(), result.getValue());
         return result;
     }

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java

@@ -2,7 +2,9 @@
 
 import liquidjava.diagnostics.DebugLog;
 import liquidjava.processor.context.Context;
+import liquidjava.processor.context.GhostState;
 import liquidjava.rj_language.Predicate;
+import java.util.List;
 import java.util.Map;
 
 import liquidjava.processor.facade.AliasDTO;
@@ -23,9 +25,10 @@ public class ExpressionSimplifier {
      * Simplifies an expression by applying constant propagation, constant folding, removing redundant conjuncts and
      * expanding aliases Returns a derivation node representing the tree of simplifications applied
      */
-    public static ValDerivationNode simplify(Expression exp, Map<String, AliasDTO> aliases) {
+    public static ValDerivationNode simplify(Expression exp, Map<String, AliasDTO> aliases,
+            List<GhostState> ghostStates) {
         DebugLog.simplificationStart(exp);
-        ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp);
+        ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp, ghostStates);
         DebugLog.simplificationPass("fixed-point reached", fixedPoint.getValue());
         ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint);
         DebugLog.simplificationPass("remove redundant &&", simplified.getValue());
@@ -36,16 +39,21 @@ public static ValDerivationNode simplify(Expression exp, Map<String, AliasDTO> a
         return expanded;
     }
 
+    public static ValDerivationNode simplify(Expression exp, Map<String, AliasDTO> aliases) {
+        return simplify(exp, aliases, List.of());
+    }
+
     public static ValDerivationNode simplify(Expression exp) {
-        return simplify(exp, Map.of());
+        return simplify(exp, Map.of(), List.of());
     }
 
     /**
      * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the
      * expression simplifies to a boolean literal, which means we've simplified too much.
      */
-    private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) {
-        ValDerivationNode simplified = simplifyOnce(current, prevExp);
+    private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp,
+            List<GhostState> ghostStates) {
+        ValDerivationNode simplified = simplifyOnce(current, prevExp, ghostStates);
         Expression currExp = simplified.getValue();
 
         // fixed point reached — compare on toString() because propagate/fold/reduce mutate the AST in place, so a
@@ -60,15 +68,25 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current,
         }
 
         // continue simplifying
-        return simplifyToFixedPoint(simplified, simplified.getValue());
+        return simplifyToFixedPoint(simplified, simplified.getValue(), ghostStates);
     }
 
-    private static ValDerivationNode simplifyOnce(ValDerivationNode current, Expression prevExp) {
-        ValDerivationNode prop = VariablePropagation.propagate(prevExp, current);
+    private static ValDerivationNode simplifyOnce(ValDerivationNode current, Expression prevExp,
+            List<GhostState> ghostStates) {
+        // Propagation is told not to collapse ghost-state equalities (stateN(x) -> stateN(y)): otherwise a
+        // chain state1(a)==state1(b) && state1(b)==state1(c) would lose its shared middle term before
+        // derivation could consume both links.
+        ValDerivationNode prop = VariablePropagation.propagate(prevExp, current,
+                StateDerivation.internalStateFunctions(ghostStates));
         DebugLog.simplificationPass("variable propagation", prop.getValue());
         ValDerivationNode fold = ExpressionFolding.fold(prop);
         DebugLog.simplificationPass("expression folding", fold.getValue());
-        ValDerivationNode simplified = simplifyValDerivationNode(fold);
+        // Derivation runs after folding: state conjuncts start life as unresolved ?: ternaries, and folding
+        // turns them into the concrete FunctionInvocation facts derivation matches. The surrounding
+        // fixed-point loop re-runs this pass, so equality chains resolve link by link across iterations.
+        ValDerivationNode derived = StateDerivation.derive(fold, ghostStates);
+        DebugLog.simplificationPass("state derivation", derived.getValue());
+        ValDerivationNode simplified = simplifyValDerivationNode(derived);
         DebugLog.simplificationPass("remove redundant && (loop)", simplified.getValue());
         return simplified;
     }