Add more complex examples

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufTest.java

@@ -0,0 +1,23 @@
+package testSuite.classes.bytebuf_correct;
+
+// SO 48582520 — UnsupportedOperationException at ByteBuffer.array()
+// https://stackoverflow.com/questions/48582520
+// SO class is already self-contained pure java.nio; only added the package.
+import java.nio.ByteBuffer;
+
+public class ByteBufTest {
+
+    public static final int TEST_BUFFER_SIZE = 128;
+
+    // private ByteBuffer mDirectBuffer;
+
+    public ByteBufTest() {
+        // FIX (from accepted answer): mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
+        // or guard with: if (mDirectBuffer.hasArray()) { ... }
+        ByteBuffer mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
+        // VIOLATION: a direct buffer is not array-backed -> array() throws
+        // UnsupportedOperationException.
+        byte[] buf = mDirectBuffer.array();
+        buf[1] = 100;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java

@@ -0,0 +1,41 @@
+package testSuite.classes.bytebuf_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+import java.nio.ByteBuffer;
+import java.nio.ByteOrder;
+import java.nio.CharBuffer;
+import java.nio.ShortBuffer;
+import java.nio.IntBuffer;
+import java.nio.LongBuffer;
+import java.nio.FloatBuffer;
+import java.nio.DoubleBuffer;
+
+
+@Ghost("boolean arrayBacked")
+@ExternalRefinementsFor("java.nio.ByteBuffer")
+public interface ByteBufferRefinements {
+
+    // ---- Backing array access ----
+
+    @StateRefinement(to="_ ? arrayBacked() : !arrayBacked()")
+    boolean hasArray();
+
+    @StateRefinement(from="arrayBacked()")
+    byte[] array();
+
+    @StateRefinement(from="arrayBacked()")
+    int arrayOffset();
+    
+    @Refinement("arrayBacked(_)")
+    ByteBuffer wrap(byte[] array, int offset, int length);
+
+    @Refinement("arrayBacked(_)")
+    ByteBuffer wrap(byte[] array);
+
+  }

liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java

@@ -0,0 +1,41 @@
+package testSuite.classes.bytebuf_error;
+
+// SO 48582520 — UnsupportedOperationException at ByteBuffer.array()
+// https://stackoverflow.com/questions/48582520
+// SO class is already self-contained pure java.nio; only added the package.
+import java.nio.ByteBuffer;
+
+public class ByteBufTest {
+
+    public static final int TEST_BUFFER_SIZE = 128;
+
+    // private ByteBuffer mDirectBuffer;
+
+    public ByteBufTest() {
+        // FIX (from accepted answer): mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
+        // or guard with: if (mDirectBuffer.hasArray()) { ... }
+        ByteBuffer mDirectBuffer = ByteBuffer.allocateDirect(TEST_BUFFER_SIZE);
+        // VIOLATION: a direct buffer is not array-backed -> array() throws
+        // UnsupportedOperationException.
+        byte[] buf = mDirectBuffer.array(); // State Refinement Error
+        buf[1] = 100;
+    }
+
+    public void test(ByteBuffer mDirectBuffer) {
+        printBuffer("nativeInitDirectBuffer", mDirectBuffer.array()); // State Refinement Error
+    }
+
+    private void printBuffer(String tag, byte[] buffer) {
+        StringBuffer sBuffer = new StringBuffer();
+        for (int i = 0; i < buffer.length; i++) {
+            sBuffer.append(buffer[i]);
+            sBuffer.append(" ");
+        }
+    }
+
+    public static void main(String[] args) throws Exception {
+        ByteBufTest item = new ByteBufTest();
+        ByteBuffer mDirectBuffer = ByteBuffer.allocateDirect(128);
+        item.test(mDirectBuffer);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java

@@ -0,0 +1,41 @@
+package testSuite.classes.bytebuf_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+import java.nio.ByteBuffer;
+import java.nio.ByteOrder;
+import java.nio.CharBuffer;
+import java.nio.ShortBuffer;
+import java.nio.IntBuffer;
+import java.nio.LongBuffer;
+import java.nio.FloatBuffer;
+import java.nio.DoubleBuffer;
+
+
+@Ghost("boolean arrayBacked")
+@ExternalRefinementsFor("java.nio.ByteBuffer")
+public interface ByteBufferRefinements {
+
+    // ---- Backing array access ----
+
+    @StateRefinement(to="_ ? arrayBacked() : !arrayBacked()")
+    boolean hasArray();
+
+    @StateRefinement(from="arrayBacked()")
+    byte[] array();
+
+    @StateRefinement(from="arrayBacked()")
+    int arrayOffset();
+    
+    @Refinement("arrayBacked(_)")
+    ByteBuffer wrap(byte[] array, int offset, int length);
+
+    @Refinement("arrayBacked(_)")
+    ByteBuffer wrap(byte[] array);
+
+  }

liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java

@@ -0,0 +1,28 @@
+package testSuite.classes.iterator_queue_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class):
+ * {@code hasNext} is an informative check (no state change), and {@code next} consumes one
+ * element, resetting state so a fresh check is required before the next consumption.
+ *
+ * <p>{@code java.util.Iterator} itself is an interface, and external refinements only attach to
+ * classes — Scanner gives us the same API in a class form.
+ */
+@StateSet({"hasMore", "inNext", "notInNext"})
+@ExternalRefinementsFor("java.util.Iterator")
+public interface IteratorRefinements<N> {
+
+    @StateRefinement(to = "_ --> hasMore()")
+    boolean hasNext();
+
+    @StateRefinement(from = "hasMore()", to = "inNext()")
+    N next();
+
+    @StateRefinement(from="inNext()", to="notInNext()")
+    void remove();
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java

@@ -0,0 +1,64 @@
+package testSuite.classes.iterator_queue_error;
+
+// SO 22361194 — "Iterator.remove() IllegalStateException"
+// https://stackoverflow.com/questions/22361194
+// Faithful to the question body. The asker's own (unshown) types are given
+// minimal stand-ins so the original structure compiles:
+//   - the queues qev1/qev2/qcv1/qcv2 -> a small Queue exposing enqueue()/iterator()
+//   - CInteger -> the nested class below
+// The asker catches UnsupportedOperationException, but iterator().remove()
+// before next() actually throws IllegalStateException — so the catch does NOT
+// fire. That mismatch is reproduced verbatim from the post.
+import java.util.ArrayList;
+import java.util.Date;
+import java.util.Iterator;
+
+public class IteratorRemoveBeforeNext {
+
+    static class Queue<T> implements Iterable<T> {
+        private final ArrayList<T> items = new ArrayList<>();
+        void enqueue(T item) { items.add(item); }
+        public Iterator<T> iterator() { return items.iterator(); }
+    }
+
+    static class CInteger {
+        final int value;
+        CInteger(int value) { this.value = value; }
+    }
+
+    public static void main(String[] args) {
+        Queue<Object> qev1 = new Queue<>();
+        Queue<Object> qev2 = new Queue<>();
+        Queue<Object> qcv1 = new Queue<>();
+        Queue<Object> qcv2 = new Queue<>();
+        Object ci = new CInteger(0);
+
+        try {
+            // VIOLATION: remove() before next() -> IllegalStateException
+            // (NOT UnsupportedOperationException, so this catch does not fire).
+            Iterator<Object> it = qev1.iterator();
+            it.remove(); // State Refinement Error
+        } catch (UnsupportedOperationException e) {
+            System.out.println("Calling Iterator.remove() and throwing exception.");
+        }
+
+        qev1.enqueue(ci);
+        qev2.enqueue(ci);
+        qcv1.enqueue(ci);
+        qcv2.enqueue(ci);
+
+        for (int i = 1; i < 5; i++) {
+            if (i % 2 == 0) {
+                qev1.enqueue(new CInteger(i + 1));
+                qev2.enqueue(new CInteger(i + 1));
+                qcv1.enqueue(new CInteger(i + 1));
+                qcv2.enqueue(new CInteger(i + 1));
+            } else {
+                qev1.enqueue(new Date(i * i));
+                qev2.enqueue(new Date(i * i));
+                qcv1.enqueue(new Date(i * i));
+                qcv2.enqueue(new Date(i * i));
+            }
+        }
+    }
+}

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

@@ -0,0 +1,21 @@
+package testSuite.classes.resultset_forward_correct;
+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_correct/PreparedStatementRefinements.java

@@ -0,0 +1,21 @@
+package testSuite.classes.resultset_forward_correct;
+
+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();
+}

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

@@ -0,0 +1,22 @@
+package testSuite.classes.resultset_forward_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"onlyForward", "allowsBackward"})
+@StateSet({"beforeRow", "onRow", "endRows"})
+
+@ExternalRefinementsFor("java.sql.ResultSet")
+public interface ResultSetRefinements {
+
+    @StateRefinement(to = "_ ? onRow(this) : endRows(this)")
+    boolean next();
+
+    @StateRefinement(from = "onRow(this)")
+    float getFloat(String columnIndex);
+
+    @StateRefinement(from = "allowsBackward()")
+    void beforeFirst();
+
+}

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java

@@ -0,0 +1,65 @@
+package testSuite.classes.resultset_forward_correct;
+
+
+// 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;
+import java.sql.Statement;
+
+public class ResultSetTests {
+
+     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.TYPE_SCROLL_INSENSITIVE, ResultSet.CONCUR_READ_ONLY);
+        ResultSet rs = pstat.executeQuery();
+
+        rs.beforeFirst(); // State Refinement Error
+
+        return typeID;
+    }
+
+    int login2(Connection con, String username, String password) throws SQLException {
+        int typeID = 0;
+        PreparedStatement pstat =
+                con.prepareStatement("select typeid from users where username=? and password=?", ResultSet.TYPE_SCROLL_INSENSITIVE, ResultSet.CONCUR_READ_ONLY);
+        pstat.setString(1, username);
+        pstat.setString(2, password);
+        ResultSet rs = pstat.executeQuery();
+        int rowCount = 0;
+        while (rs.next()) {
+            rowCount++;
+        }
+        rs.beforeFirst(); // State Refinement Error
+        if (rowCount >= 1) {
+            while (rs.next()) {
+                typeID = rs.getInt(1);
+            }
+        }
+        return typeID;
+    }
+
+    float readAverage(Connection conn) throws SQLException {
+        Statement parentstmt = conn.createStatement();
+        ResultSet parentMessage =
+                parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
+        // FIX (from accepted answer): parentMessage.next();
+        // VIOLATION: cursor is before the first row; getFloat() with no next().
+        if( parentMessage.next()) {
+            float avgsum = parentMessage.getFloat("IMPAVG");
+            return avgsum;
+        } else {
+            return 0.0f;
+        }
+    }
+}