diff --git a/README.md b/README.md index 5f9f1374..3fa980a2 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ You can find out more about LiquidJava in the following resources: ## Run verification #### In a specific project -Run the file `liquidjava-verifier\api\CommandLineLaucher` with the path to the target project for verification. +Run the file `liquidjava-verifier\api\CommandLineLauncher` with the path to the target project for verification. If there are no arguments given, the application verifies the project on the path `liquidjava-example\src\main\java`. diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/Account.java b/liquidjava-example/src/main/java/test/currentlyTesting/Account.java deleted file mode 100644 index 3fa8a637..00000000 --- a/liquidjava-example/src/main/java/test/currentlyTesting/Account.java +++ /dev/null @@ -1,26 +0,0 @@ -package test.currentlyTesting; - -// import liquidjava.specification.Ghost; -// import liquidjava.specification.StateRefinement; -// import liquidjava.specification.StateSet; - -// @Ghost("int amount") -// @StateSet({"positive", "negative"}) -public class Account { - // int qnt; - // - // @StateRefinement(from="positive(this)", - // to="(amount(this) == amount(old(this)) - x) && " + - // "(amount(this) < 0? negative(this):positive(this))") - //// @StateRefinement(to="(amount(this) == amount(old(this)) - x)") - // public int withdraw(int x) { - // qnt -= x; - // return qnt; - // } - // - // @StateRefinement(to="amount(this) == amount(old(this)) + x") - // public void add(int x) { - // qnt += x; - // } - -} diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java index fc8d6c5d..647a3c1c 100644 --- a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java +++ b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java @@ -4,12 +4,24 @@ class SimpleTest { - @Refinement("return > 0") + @Refinement("return < 0") public int test() { return 10; } } + + + + + + + + + + + + // @RefinementAlias("Percentage(int x) { 0 <= x && x <= 100 }") // @Refinement("Percentage(_)") // public static int addBonus( diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_forwardonly/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_forwardonly/Test.java new file mode 100644 index 00000000..ad7d389d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_forwardonly/Test.java @@ -0,0 +1,51 @@ +package testSuite.in_progress.searching_state_space.resultset_forwardonly; + +import java.sql.Connection; +import java.sql.PreparedStatement; +import java.sql.ResultSet; + +/** + * ResultSet + */ +public class Test { + + /* + * Error ResultSet is FORWARD_ONLY and we try to get a value before + */ + public static void example6367737(Connection con, String username, String password ) throws Exception { + + // Step 1) Prepare the statement + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?"); + + // Step 2) Set parameters for the statement + pstat.setString(1, username); + pstat.setString(2, password); + + // Step 3) Execute the query + ResultSet rs = pstat.executeQuery(); + + // Step 4) Process the result + int rowCount=0; + while(rs.next()){ + rowCount++; + } + + // ERROR! because it is FORWARD_ONLY, we cannot go back and check beforeFirst + rs.beforeFirst(); + + int typeID = 0; + if(rowCount>=1) { + while(rs.next()){ + typeID=rs.getInt(1); + } + } + + // To be correct we need to change the resultset to be scrollable + /*PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?", + ResultSet.TYPE_SCROLL_SENSITIVE, + ResultSet.CONCUR_UPDATABLE); + */ + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_read_after_end/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_read_after_end/Test.java new file mode 100644 index 00000000..efbc7a30 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_read_after_end/Test.java @@ -0,0 +1,24 @@ +package testSuite.in_progress.searching_state_space.resultset_read_after_end; + +import java.sql.ResultSet; + +/** + * URLConnection + */ +public class Test { + + /* + * Error cannot reschedule a timer + */ + public static Object example1801324(ResultSet rs) throws Exception { + Object count = null; + if (rs != null) { + while (rs.next()) { + count = rs.getInt(1); + } + count = rs.getInt(1); //this will throw Exhausted resultset + } + + return count; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_read_before_next/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_read_before_next/Test.java new file mode 100644 index 00000000..07e73d0f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/resultset_read_before_next/Test.java @@ -0,0 +1,32 @@ +package testSuite.in_progress.searching_state_space.resultset_read_before_next; + +import java.sql.Connection; +import java.sql.PreparedStatement; +import java.sql.ResultSet; + +/** + * ResultSet + */ +public class Test { + + /* + * Error - in ResultSet, after executing the query we need to call next() before getting a value + */ + public static void example6367737(Connection con, String username, String password ) throws Exception { + + // Step 1) Prepare the statement + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?"); + + // Step 2) Set parameters for the statement + pstat.setString(1, username); + pstat.setString(2, password); + + // Step 3) Execute the query + ResultSet parentMessage = pstat.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + + float avgsum = parentMessage.getFloat("IMPAVG"); // Error because we are trying to get a value before next + + // To be correct we need to call next() before the getter + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/timertask_cannot_reschedule/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/timertask_cannot_reschedule/Test.java new file mode 100644 index 00000000..48eec259 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/timertask_cannot_reschedule/Test.java @@ -0,0 +1,33 @@ +package testSuite.in_progress.searching_state_space.timertask_cannot_reschedule; + +import java.util.Map; +import java.util.Timer; +import java.util.TimerTask; + +/** + * URLConnection + * + * -> STATE_OPENED -> STATE_SETTER -> STATE_CONNECTED + */ +public class Test { + + /* + * Error cannot reschedule a timer + */ + public static void example1801324( Map timers, String sessionKey) { + + // Step 1) Get the timer + Timer timer = timers.get(sessionKey); + + // Step 2) Cancel the timer + timer.cancel(); + + // Step 3) Schedule a new task for this timer -> ERROR Cannot reschedule a Timer + timer.schedule(new TimerTask() { + @Override + public void run() { + System.out.println("Timer task completed."); + } + }, 1000); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/url_connection_reuse_connection/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/url_connection_reuse_connection/Test.java new file mode 100644 index 00000000..5e1ff5e3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/url_connection_reuse_connection/Test.java @@ -0,0 +1,37 @@ +package testSuite.in_progress.searching_state_space.url_connection_reuse_connection; + +import java.io.IOException; +import java.net.URL; +import java.net.URLConnection; + +/** + * URLConnection + * + * -> STATE_OPENED -> STATE_SETTER -> STATE_CONNECTED + */ +public class Test { + /* + * Error cannot set property before opening connection + */ + public static void example4278917(URL address) { + try { + + // Step 1) Open the connection + URLConnection connection = address.openConnection(); + + // Step 2) Connect + connection.connect(); + + /* Other code in original question */ + + // Step 3) Setup parameters and connection properties after connection == ERROR + connection.setAllowUserInteraction(true); + connection.addRequestProperty("AUTHENTICATION_REQUEST_PROPERTY", "authorizationRequest"); + connection.getHeaderFields(); + + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/url_connection_set_property/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/url_connection_set_property/Test.java new file mode 100644 index 00000000..3ae50cd2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/searching_state_space/url_connection_set_property/Test.java @@ -0,0 +1,98 @@ +package testSuite.in_progress.searching_state_space.url_connection_set_property; + +import java.io.InputStream; +import java.io.OutputStream; +import java.io.IOException; +import java.net.HttpURLConnection; +import java.net.URL; +import java.net.URLConnection; + +public class Test { + public static void example331538(URL address) { + try { + + // Step 1) Open the connection + URLConnection cnx = address.openConnection(); + + // Step 2) Setup parameters and connection properties + cnx.setAllowUserInteraction(false); // Step 2) + cnx.setDoOutput(true); + cnx.addRequestProperty("User-Agent", + "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)"); + + + // Step 3) + cnx.connect(); + + // Step 4) + cnx.getContent(); + + // Get the input stream and process it + InputStream is = cnx.getInputStream(); + System.out.println("Successfully opened input stream."); + + // Ensure to close the InputStream after use + is.close(); + + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } + + + /** + * + */ + String sessionId = "1234"; + public void example5368535(URL address, String content) { + try { + HttpURLConnection con = openConnection(address, true, true, "POST"); + + //ERROR write before set + writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() + setCookies(con); // writeOutput calls cnx.setRequestProperty + + con.connect(); + + System.out.println("Request completed successfully."); + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } + + // Exactly from the original code + public static final HttpURLConnection openConnection(URL url, boolean in, boolean out,String requestMethode) throws IOException{ + HttpURLConnection con = (HttpURLConnection) url.openConnection (); + con.setDoInput(in); + con.setDoOutput (out); + if(requestMethode == null){ + requestMethode = "GET"; + } + con.setRequestMethod(requestMethode); + con.setRequestProperty ("Content-Type", "application/x-www-form-urlencoded"); + return con; + } + + // Set cookies + private void setCookies(HttpURLConnection cnx) { + if (sessionId != null) { + cnx.setRequestProperty("Cookie", sessionId); + System.out.println("Cookie set: " + sessionId); + } + } + + // Write content + private void writeToOutput(HttpURLConnection cnx, String content) throws IOException { + try { + OutputStream os = cnx.getOutputStream() ; + os.write(content.getBytes()); + os.flush(); + os.close(); + } catch (IOException e) { + System.err.println("Error writing content: " + e.getMessage()); + throw e; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/file_input_stream_not_tested/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/file_input_stream_not_tested/Test.java new file mode 100644 index 00000000..c6e812f3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/file_input_stream_not_tested/Test.java @@ -0,0 +1,54 @@ +package testSuite.in_progress.stack_overflow.file_input_stream_not_tested; + +import java.io.File; +import java.io.FileInputStream; +import java.io.IOException; +import java.util.Deque; +import java.util.Iterator; +import java.util.LinkedList; +import java.util.Queue; +import java.io.File; +import java.io.FileInputStream; +import java.io.IOException; + + + +/** + * Examples related to typestate refinements. + * Idea from: https://stackoverflow.com/questions/5900435/blackberry-fileconnection-illegalstateexception + * I am not sure we can handle this case since testFile does not need to know about FileInputStream, it is only used as a parameter. + * Can we still relate them? Does it make sense? + * + * In a way similar to https://stackoverflow.com/questions/15609033/causes-for-illegalstateexception + */ +@SuppressWarnings("unused") +public class Test { + + public static void main(String[] args) { + + // Create a test file + File testFile = new File("liquidjava-example/src/main/java/testSuite/classes/stack_overflow/file_input_stream/testFile.txt"); + + // Simulate opening the file and forgetting to close it + FileInputStream inputStream = null; + try { + // Open the file + inputStream = new FileInputStream(testFile); + System.out.println("Reading the file..."); + + Thread.sleep(500); // Simulating a delay + + // inputStream.close(); // Error: Should be here to fix the issue + + } catch (IOException | InterruptedException e) { + e.printStackTrace(); + } + + // Attempt to delete the file (this will fail if the file is still open) + if (testFile.delete()) { + System.out.println("File deleted successfully."); + } else { + System.out.println("Failed to delete the file. It might be open."); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/file_input_stream_not_tested/testFile.txt b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/file_input_stream_not_tested/testFile.txt new file mode 100644 index 00000000..63c0b754 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/file_input_stream_not_tested/testFile.txt @@ -0,0 +1 @@ +qegigduaskxjnlm, \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/HttpEntity.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/HttpEntity.java new file mode 100644 index 00000000..c757cd18 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/HttpEntity.java @@ -0,0 +1,11 @@ +package testSuite.in_progress.stack_overflow.httpEntity; + +import java.io.InputStream; + +public class HttpEntity { + + // TODO: STUB METHOD + public InputStream getContent() { + return (InputStream) new Object(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/HttpResponse.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/HttpResponse.java new file mode 100644 index 00000000..003a736d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/HttpResponse.java @@ -0,0 +1,9 @@ +package testSuite.in_progress.stack_overflow.httpEntity; + +public class HttpResponse { + + // TODO: STUB METHOD + public HttpEntity getEntity() { + return new HttpEntity(); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/Test.java new file mode 100644 index 00000000..7e25d275 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/httpEntity/Test.java @@ -0,0 +1,18 @@ +package testSuite.in_progress.stack_overflow.httpEntity; + +import java.io.BufferedReader; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.io.UnsupportedEncodingException; + +public class Test { + public static void test(HttpResponse r) throws UnsupportedEncodingException { + HttpResponse response = r; + InputStream in = response.getEntity().getContent(); + BufferedReader reader = new BufferedReader( + new InputStreamReader( + response.getEntity().getContent(), "UTF-8")); // Second call to getEntity() + + //Cannot call getContent twice if the entity is not repeatable. There is a method isRepeatable() to check + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/IteratorRefinements.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/IteratorRefinements.java new file mode 100644 index 00000000..aa737d48 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/IteratorRefinements.java @@ -0,0 +1,23 @@ +package testSuite.in_progress.stack_overflow.iterator_not_tested; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + +@ExternalRefinementsFor("java.util.Iterator") +@StateSet({"start", "ready", "inNext"}) +public interface IteratorRefinements { + + @StateRefinement(to = "start(this)") + public void Iterator(); + + @StateRefinement(to = "ready(this)") + public boolean hasNext(); + + @StateRefinement(from = "ready(this)", to = "inNext(this)") + public Object next(); + + @StateRefinement(from = "inNext(this)", to = "start(this)") + public void remove(); +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/LinkedListRefinements.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/LinkedListRefinements.java new file mode 100644 index 00000000..29b8cd34 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/LinkedListRefinements.java @@ -0,0 +1,15 @@ +package testSuite.in_progress.stack_overflow.iterator_not_tested; + +import java.util.Iterator; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; + +@ExternalRefinementsFor("java.util.LinkedList") +public interface LinkedListRefinements { + + @Refinement("init(_)")//? or just assume its correct + public Iterator iterator(); + + +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/TestIterator.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/TestIterator.java new file mode 100644 index 00000000..7bb751d7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/iterator_not_tested/TestIterator.java @@ -0,0 +1,77 @@ +package testSuite.in_progress.stack_overflow.iterator_not_tested; + +import java.util.Deque; +import java.util.Iterator; +import java.util.LinkedList; +import java.util.Queue; +/** + * Examples related to Iterator typestate refinements. + * Ideas from: https://stackoverflow.com/questions/22361194/iterator-remove-illegalstateexception + */ +@SuppressWarnings("unused") +public class TestIterator { + + public static void main(String[] args) { + + // Define and initialize queues + Queue qev1, qev2, qcv1, qcv2; + qev1 = new LinkedList<>(); + qev2 = new LinkedList<>(); + qcv1 = new LinkedList<>(); + qcv2 = new LinkedList<>(); + + qev1.add(100); + qev1.add(200); + qev1.add(300); + qev1.add(300); + qev1.add(300); + qev1.add(300); + + // Get an iterator for the queue + Iterator iterator = qev1.iterator(); + + try { + iterator.remove(); // Error no call to next before remove + } + catch(UnsupportedOperationException e) { + System.out.println("Calling Iterator.remove() and throwing exception."); + } + + } + + public static void testWrong(String[] args) { + + // Define and initialize queues + Queue qev1, qev2, qcv1, qcv2; + qev1 = new LinkedList<>(); + qev2 = new LinkedList<>(); + qcv1 = new LinkedList<>(); + qcv2 = new LinkedList<>(); + + qev1.add(100); + qev1.add(200); + qev1.add(300); + qev1.add(300); + qev1.add(300); + qev1.add(300); + + // Get an iterator for the queue + Iterator iterator = qev1.iterator(); + + try { + iterator.hasNext(); + iterator.next(); + if (iterator.hasNext()){ + iterator.next(); + iterator.hasNext(); + iterator.next(); + } + iterator.remove(); // No error + iterator.remove(); // Error: needs to have + } + catch(UnsupportedOperationException e) { + System.out.println("Calling Iterator.remove() and throwing exception."); + } + + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/maps_marker/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/maps_marker/Test.java new file mode 100644 index 00000000..76a50d91 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/maps_marker/Test.java @@ -0,0 +1,37 @@ +package testSuite.in_progress.stack_overflow.maps_marker; +public class Test { + + void createMarker(GoogleMap map) { + MarkerOptions options = new MarkerOptions(); + // options.position(new LatLng(lat, lang)); //NEEDED + // options.anchor() + + System.out.println("LazyMarker - Options var val: "+options.toString()); + System.out.println("LazyMarker - GoogleMap Value:"+map.toString()); + var marker = map.addMarker(options); + + System.out.println("LazyMarker - GoogleMap Marker:"+marker.toString()); + + } + + + /* + * STUB CLASSES + */ + class GoogleMap { + public Marker addMarker(MarkerOptions options) { + return new Marker(); + } + } + + class Marker { + public Marker(){} + } + + class MarkerOptions { + } + + + +} + diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/mediaRecord/MediaRecorder.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/mediaRecord/MediaRecorder.java new file mode 100644 index 00000000..581fbe86 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/mediaRecord/MediaRecorder.java @@ -0,0 +1,50 @@ +package testSuite.in_progress.stack_overflow.mediaRecord; +/* + * Mock class for MediaRecorder Android + * https://developer.android.com/reference/android/media/MediaRecorder + */ +public class MediaRecorder { + + public static final String AudioSource = null; + + public void start() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'start'"); + } + + public void stop() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'stop'"); + } + + public void setAudioSource() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'setAudioSource'"); + } + + public void setOutputFormat() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'setOutputFormat'"); + } + + public void setAudioEncoder() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'setAudioEncoder'"); + } + + public void setOutputFile() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'setOutputFile'"); + } + + public void setVideoSource() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'setVideoSource'"); + } + + public void setProfile() { + // TODO Auto-generated method stub + throw new UnsupportedOperationException("Unimplemented method 'setProfile'"); + } + +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/mediaRecord/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/mediaRecord/Test.java new file mode 100644 index 00000000..b28c9524 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/mediaRecord/Test.java @@ -0,0 +1,32 @@ +package testSuite.in_progress.stack_overflow.mediaRecord; + +public class Test { + public static void test( boolean isChecked) { + MediaRecorder recorder = new MediaRecorder(); + + recorder.setAudioSource(); + recorder.setOutputFormat(); + recorder.setAudioEncoder(); + recorder.setOutputFile(); + + while (isChecked) { // While loop will make it start and stop multiple times + recorder.start(); // here it were it throws + //... + recorder.stop(); + } + + } + + + public static void test2( boolean isChecked) { + MediaRecorder recorder = new MediaRecorder(); + + recorder.setAudioSource(); + recorder.setVideoSource(); + recorder.setOutputFormat(); + recorder.setProfile(); // setProfile error + // From stackoverflow - setProfile() tries to setOutput but cannot because it is already explicitly set - which makes it redundant + // From documentation - setProfile() should be done after setAudioSource and setVideoSource and after should be setOutputFile - however, it does not appear in the SM + + } +} diff --git a/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/random/Test.java b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/random/Test.java new file mode 100644 index 00000000..8ea4249f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/in_progress/stack_overflow/random/Test.java @@ -0,0 +1,19 @@ +package testSuite.in_progress.stack_overflow.random; + +import java.util.ArrayList; +import java.util.Date; +import java.util.Random; + +public class Test { + + public static String extractIndividualInstance(ArrayList instances) { + Random generator = new Random(new Date().getTime()); + int random = generator.nextInt(instances.size() - 1); // if size is 0 throws exception + + String singleInstance = instances.get(random); + instances.remove(random); + + return singleInstance; + } + +} diff --git a/liquidjava-example/src/main/java/testingInProgress/Account.java b/liquidjava-example/src/main/java/testingInProgress/Account.java index e7d90423..f0ed3d62 100644 --- a/liquidjava-example/src/main/java/testingInProgress/Account.java +++ b/liquidjava-example/src/main/java/testingInProgress/Account.java @@ -1,42 +1,26 @@ package testingInProgress; -import liquidjava.specification.Ghost; -import liquidjava.specification.Refinement; -import liquidjava.specification.StateRefinement; +// import liquidjava.specification.Ghost; +// import liquidjava.specification.StateRefinement; +// import liquidjava.specification.StateSet; -@Ghost("int sum") +// @Ghost("int amount") +// @StateSet({"positive", "negative"}) public class Account { - - @Refinement("balance >= 0") - private int balance; - - public Account() { - balance = 0; - } - - @StateRefinement(to = "sum(this) == v") - public Account(@Refinement("v >= 0") int v) { - balance = v; - } - - @StateRefinement( - to = "(sum(old(this)) > v)? (sum(this) == (sum(old(this)) - v)) : (sum(this) == 0)") - public void withdraw(int v) { - if (v > balance) balance = 0; - else balance = balance - v; - } - - @StateRefinement(to = "sum(this) == (sum(old(this)) + v)") - public void deposit(int v) { - balance += v; - } - - // @StateRefinement(from="(amount <= sum(this)) && (sum(this) == sum(old(this)))", to="...") - // @Refinement("sum(_) == (sum(old(_)) + amount)") - // public Account transferTo(Account other, @Refinement("_ < sum(this)")int amount) { - // this.withdraw(amount); - // other.deposit(amount); - // return other; - // } + // int qnt; + // + // @StateRefinement(from="positive(this)", + // to="(amount(this) == amount(old(this)) - x) && " + + // "(amount(this) < 0? negative(this):positive(this))") + //// @StateRefinement(to="(amount(this) == amount(old(this)) - x)") + // public int withdraw(int x) { + // qnt -= x; + // return qnt; + // } + // + // @StateRefinement(to="amount(this) == amount(old(this)) + x") + // public void add(int x) { + // qnt += x; + // } } diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/AccountClient.java b/liquidjava-example/src/main/java/testingInProgress/AccountClient.java similarity index 91% rename from liquidjava-example/src/main/java/test/currentlyTesting/AccountClient.java rename to liquidjava-example/src/main/java/testingInProgress/AccountClient.java index 9c7d88a8..723055ce 100644 --- a/liquidjava-example/src/main/java/test/currentlyTesting/AccountClient.java +++ b/liquidjava-example/src/main/java/testingInProgress/AccountClient.java @@ -1,4 +1,4 @@ -package test.currentlyTesting; +package testingInProgress; // @StateSet({"active", "inactive"}) public class AccountClient { diff --git a/liquidjava-example/src/main/java/testingInProgress/CommitAndRedirectSimulation.java b/liquidjava-example/src/main/java/testingInProgress/CommitAndRedirectSimulation.java new file mode 100644 index 00000000..91f92df5 --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/CommitAndRedirectSimulation.java @@ -0,0 +1,95 @@ +package testingInProgress; + +import java.io.PrintWriter; + +/** + * This class simulates the HttpServletResponse object, which handles writing to the response and sending redirects. + * Main class to simulate and test the commit and redirect behavior. + */ +public class CommitAndRedirectSimulation { + + public static void main(String[] args) { + // Create a simulated HTTP response + HttpServletResponseMock response = new HttpServletResponseMock(); + // Call the logic that mimics a real servlet behavior + new CommitAndRedirectExample().doGet(response); + } +} + + +class CommitAndRedirectExample { + + /** + * Simulates the logic of handling an HTTP GET request, including writing content to + * the response and attempting a redirect. If the response has been committed, + * a redirection will throw an {@link IllegalStateException}. + * + * @param response The simulated HTTP response. + */ + public void doGet(HttpServletResponseMock response) { + // Write some content to the response (this will commit the response) + PrintWriter out = response.getWriter(); + // out.println("This is some content that will be sent to the client."); + + // At this point, the response is committed (content is already sent to the client) + + // Try to send a redirect after the response has been committed + + response.sendRedirect("http://example.com"); + System.out.println("Redirect attempted."); + } +} + +/** + * This class simulates the HttpServletResponse object, which handles writing to the response and sending redirects. + * Simulates the {@link HttpServletResponse} object for testing purposes. + * It mimics the behavior of response commitment and the ability to perform redirection. + */ +class HttpServletResponseMock { + private boolean committed = false; + private PrintWriter writer; + + /** + * Constructor that initializes the mock response writer to print to the console. + */ + public HttpServletResponseMock() { + this.writer = new PrintWriter(System.out); // Write to standard output for simulation + } + + /** + * Returns a {@link PrintWriter} for writing content to the response. + * If the response hasn't been committed before, it marks the response as committed. + * + * @return The {@link PrintWriter} for writing content. + */ + public PrintWriter getWriter() { + if (!committed) { + committed = true; // Once content is written, the response is considered committed + } + return writer; + } + + /** + * Simulates sending a redirect response to the client. + * If the response is already committed, an {@link IllegalStateException} is thrown. + * + * @param url The URL to redirect the client to. + * @throws IllegalStateException if the response is already committed. + */ + public void sendRedirect(String url) { + if (committed) { + throw new IllegalStateException("Cannot call sendRedirect() after the response has been committed."); + } + // In a real servlet, it would set the HTTP status and Location header here + System.out.println("Redirecting to: " + url); + } + + /** + * Returns whether the response has already been committed (i.e., content has been written). + * + * @return True if the response has been committed, false otherwise. + */ + public boolean isCommitted() { + return committed; + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/IteratorRefinements.java b/liquidjava-example/src/main/java/testingInProgress/IteratorRefinements.java new file mode 100644 index 00000000..ba8d0bc3 --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/IteratorRefinements.java @@ -0,0 +1,23 @@ +package testingInProgress; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + +@ExternalRefinementsFor("java.util.Iterator") +@StateSet({"start", "ready", "inNext"}) +public interface IteratorRefinements { + + @StateRefinement(to = "start(this)") + public void Iterator(); + + @StateRefinement(to = "ready(this)") + public boolean hasNext(); + + @StateRefinement(from = "ready(this)", to = "inNext(this)") + public Object next(); + + @StateRefinement(from = "inNext(this)", to = "start(this)") + public void remove(); +} diff --git a/liquidjava-example/src/main/java/testingInProgress/LinkedListRefinements.java b/liquidjava-example/src/main/java/testingInProgress/LinkedListRefinements.java new file mode 100644 index 00000000..c0a1d399 --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/LinkedListRefinements.java @@ -0,0 +1,15 @@ +package testingInProgress; + +import java.util.Iterator; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; + +@ExternalRefinementsFor("java.util.LinkedList") +public interface LinkedListRefinements { + + @Refinement("init(_)")//? or just assume its correct + public Iterator iterator(); + + +} diff --git a/liquidjava-example/src/main/java/testingInProgress/TestIterator.java b/liquidjava-example/src/main/java/testingInProgress/TestIterator.java new file mode 100644 index 00000000..db70e47f --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/TestIterator.java @@ -0,0 +1,55 @@ +package testingInProgress; + +import java.io.File; +import java.io.FileInputStream; +import java.io.IOException; +import java.util.Deque; +import java.util.Iterator; +import java.util.LinkedList; +import java.util.Queue; +import java.io.File; +import java.io.FileInputStream; +import java.io.IOException; + + + +/** + * Examples related to typestate refinements. + * Idea from: https://stackoverflow.com/questions/5900435/blackberry-fileconnection-illegalstateexception + * I am not sure we can handle this case since testFile does not need to know about FileInputStream, it is only used as a parameter. + * Can we still relate them? Does it make sense? + */ +@SuppressWarnings("unused") +public class TestIterator { + + public static void main(String[] args) { + + // Create a test file + File testFile = new File("liquidjava-example/src/main/java/test/currentlyTesting/testFile.txt"); + + // Simulate opening the file and forgetting to close it + FileInputStream inputStream = null; + try { + // Open the file + inputStream = new FileInputStream(testFile); + System.out.println("Reading the file..."); + + // Simulate a long operation without closing the file + // Note: Normally, you'd process the file here, but we're just mimicking the issue + Thread.sleep(500); // Simulating a delay + + // We forget to close the file here, mimicking the problem + // inputStream.close(); // Error: Should be here to fix the issue + + } catch (IOException | InterruptedException e) { + e.printStackTrace(); + } + + // Attempt to delete the file (this will fail if the file is still open) + if (testFile.delete()) { + System.out.println("File deleted successfully."); + } else { + System.out.println("Failed to delete the file. It might be open."); + } + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/testFile.txt b/liquidjava-example/src/main/java/testingInProgress/testFile.txt new file mode 100644 index 00000000..63c0b754 --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/testFile.txt @@ -0,0 +1 @@ +qegigduaskxjnlm, \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index dfb6ae3a..3007b4d0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -10,7 +10,8 @@ public class CommandLineLauncher { public static void main(String[] args) { - String allPath = "./liquidjava-example/src/main/java/test/currentlyTesting"; + String allPath //= "./liquidjava-example/src/main/java/test/currentlyTesting"; + = "/Users/cgamboa/git/liquidjava-examples/part3-liquidJava/together1/src"; // String allPath = "C://Regen/test-projects/src/Main.java"; // In eclipse only needed this:"../liquidjava-example/src/main/java/" diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index 9345a6d0..dde5a751 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -27,7 +27,7 @@ public class TestExamples { @MethodSource("fileNameSource") public void testFile(final Path filePath) { String fileName = filePath.getFileName().toString(); - + // 1. Run the verifier on the file or package ErrorEmitter errorEmitter = CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString());