new example to fix

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ConnectionRefinements.java

@@ -0,0 +1,21 @@
+package testSuite.classes.resultset_forward_error;
+import java.sql.PreparedStatement;
+import java.sql.ResultSet;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+
+
+@ExternalRefinementsFor("java.sql.Connection")
+public interface ConnectionRefinements {
+
+    // Default statements are forward-only: the produced ResultSet cannot scroll backwards.
+    @Refinement("setBackwards(_) == false")
+    PreparedStatement prepareStatement(String sql);
+
+    // Explicit type decides scrollability: only TYPE_FORWARD_ONLY forbids backward scrolling.
+    @Refinement("resultSetType == ResultSet.TYPE_FORWARD_ONLY ? setBackwards(_) == false : setBackwards(_) == true")
+    PreparedStatement prepareStatement(String sql, int resultSetType,
+                                       int resultSetConcurrency);
+
+ }

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java

@@ -0,0 +1,21 @@
+package testSuite.classes.resultset_forward_error;
+
+import java.sql.ResultSet;
+import java.sql.SQLException;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+
+@Ghost("boolean setBackwards")
+@ExternalRefinementsFor("java.sql.PreparedStatement")
+public interface PreparedStatementRefinements {
+
+    // The ResultSet inherits the statement's scrollability: backward-capable statements
+    // yield an allowsBackward ResultSet, forward-only statements yield an onlyForward one.
+    @Refinement("setBackwards(this) ? allowsBackward(_) : onlyForward(_)")
+    ResultSet executeQuery() throws SQLException;
+}

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetBeforeFirstOnForwardOnly.java

@@ -0,0 +1,36 @@
+package testSuite.classes.resultset_forward_error;
+
+
+// SO 6367737 — "ResultSet: Exception: set type is TYPE_FORWARD_ONLY -- why?"
+// https://stackoverflow.com/questions/6367737
+// Counting rows by iterating, then calling rs.beforeFirst() to rewind and iterate
+// again. A default ResultSet is TYPE_FORWARD_ONLY, so the backward scroll throws:
+//     java.sql.SQLException: Result set type is TYPE_FORWARD_ONLY
+//         at ...JdbcOdbcResultSet.beforeFirst(...)
+// Kept as close to the question as possible; the SO lines are wrapped in a method
+// taking a Connection. Pure java.sql; compiles with no JDBC driver present.
+import java.sql.Connection;
+import java.sql.PreparedStatement;
+import java.sql.ResultSet;
+import java.sql.SQLException;
+
+public class ResultSetBeforeFirstOnForwardOnly {
+
+     int login(Connection con, String username, String password) throws SQLException {
+        int typeID = 0;
+
+        PreparedStatement pstat =
+                con.prepareStatement("select typeid from users where username=? and password=?");
+        ResultSet rs = pstat.executeQuery();
+
+        // The default ResultSet is TYPE_FORWARD_ONLY, so the next line cannot rewind:
+        // beforeFirst() requires a scrollable (allowsBackward) ResultSet.
+        // FIX (accepted answers): request a scrollable result set, e.g.
+        //   con.prepareStatement(sql, ResultSet.TYPE_SCROLL_INSENSITIVE,
+        //                             ResultSet.CONCUR_READ_ONLY);
+        // or drop the rewind and read typeID inside the single forward pass.
+        rs.beforeFirst(); // State Refinement Error
+
+        return typeID;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetRefinements.java

@@ -0,0 +1,19 @@
+package testSuite.classes.resultset_forward_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"onlyForward", "allowsBackward"})
+
+@ExternalRefinementsFor("java.sql.ResultSet")
+public interface ResultSetRefinements {
+
+    boolean next();
+
+    float getFloat(String columnIndex);
+
+    @StateRefinement(from = "allowsBackward()")
+    void beforeFirst();
+
+}