Skip to content

Commit 2df34cc

Browse files
CatarinaGamboaCatarinaGamboa
committed
add example for urlconnection reuse
1 parent 2d3aa3e commit 2df34cc

9 files changed

Lines changed: 644 additions & 0 deletions

‎latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
package examples;
2+
3+
4+
import java.util.TimerTask;
5+
6+
import specification.Borrowed;
7+
import specification.Free;
8+
import specification.Unique;
9+
10+
public class ResultSetForwardOnly {
11+
/*
12+
* Error ResultSet is FORWARD_ONLY and we try to get a value before
13+
*/
14+
public static void example6367737(Connection con, String username, String password ) throws Exception {
15+
16+
// Step 1) Prepare the statement
17+
PreparedStatement pstat =
18+
con.prepareStatement("select typeid from users where username=? and password=?");
19+
20+
// Step 2) Set parameters for the statement
21+
pstat.setString(1, username);
22+
pstat.setString(2, password);
23+
24+
// Step 3) Execute the query
25+
ResultSet rs = pstat.executeQuery();
26+
27+
// Step 4) Process the result
28+
int rowCount=0;
29+
while(rs.next()){
30+
rowCount++;
31+
}
32+
33+
// ERROR! because it is FORWARD_ONLY, we cannot go back and check beforeFirst
34+
rs.beforeFirst();
35+
36+
int typeID = 0; // ...
37+
38+
// To be correct we need to change the resultset to be scrollable
39+
/*PreparedStatement pstat =
40+
con.prepareStatement("select typeid from users where username=? and password=?",
41+
ResultSet.TYPE_SCROLL_SENSITIVE,
42+
ResultSet.CONCUR_UPDATABLE);
43+
*/
44+
}
45+
46+
47+
class Connection{
48+
49+
// Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY
50+
// and have a concurrency level of CONCUR_READ_ONLY.
51+
@Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY")
52+
public PreparedStatement prepareStatement(String s) {
53+
return new PreparedStatement();
54+
}
55+
56+
@Unique // @StateRefinement (return, to="type == resultSetType")
57+
public PreparedStatement prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){
58+
return new PreparedStatement();
59+
60+
}
61+
}
62+
63+
// @Ghost("type")
64+
class PreparedStatement{
65+
66+
void setString(int index, String s){}
67+
68+
// @StateRefinement(return, to="type != TYPE_FORWARD_ONLY, col == -1")
69+
ResultSet executeQuery(String s){return null;}
70+
71+
// @StateRefinement(return, to="type, col == -1")
72+
ResultSet executeQuery(){return null;}
73+
}
74+
75+
// @Ghost("type")
76+
class ResultSet{
77+
78+
// @StateRefinement(this, type == )
79+
void beforeFirst(){}
80+
81+
// @StateRefinement(this, col > 0)
82+
float getFloat(String s){return 0;}
83+
84+
// @StateRefinement(this, col > 0)
85+
int getInt(int s){return 0;}
86+
87+
// @StateRefinement(this, col == old(col) + 1)
88+
boolean next(){return true;}
89+
}
90+
91+
92+
}
93+
94+

‎latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
2+
import java.util.TimerTask;
3+
4+
import specification.Borrowed;
5+
import specification.Free;
6+
import specification.Unique;
7+
8+
public class SSSResultSetNoNext {
9+
10+
11+
/*
12+
* Error - in ResultSet, after executing the query we need to call next() before getting a value
13+
*/
14+
public static void example6367737(@Borrowed Connection con, String username, String password ) throws Exception {
15+
16+
// Step 1 Prepare the statement
17+
PreparedStatement pstat =
18+
con.prepareStatement("select typeid from users where username=? and password=?");
19+
20+
// Step 2 Set parameters for the statement
21+
pstat.setString(1, username);
22+
pstat.setString(2, password);
23+
24+
// Step 3 Execute the query
25+
ResultSet parentMessage = pstat.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
26+
27+
float avgsum = parentMessage.getFloat("IMPAVG"); // Error because we are trying to get a value before next
28+
// To be correct we need to call next() before the getter
29+
}
30+
31+
32+
class Connection{
33+
34+
// Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY
35+
// and have a concurrency level of CONCUR_READ_ONLY.
36+
@Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY")
37+
public PreparedStatement prepareStatement(String s) {
38+
return new PreparedStatement();
39+
}
40+
41+
// To change resultSetType
42+
// prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){}
43+
}
44+
45+
class PreparedStatement{
46+
void setString(int index, String s){}
47+
48+
// @ReturnState( to="TYPE_FORWARD_ONLY, beforeRow")
49+
ResultSet executeQuery(String s){return null;}
50+
}
51+
52+
//@StateSet({"beforeRow", "onRow"})
53+
class ResultSet{
54+
// @StateRefinement( from = "onRow")
55+
float getFloat(String s){return 0;}
56+
57+
// @StateRefinement( to="onRow")
58+
void next(){}
59+
}
60+
61+
62+
}
63+
64+

‎latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
import java.util.TimerTask;
2+
3+
import specification.Borrowed;
4+
import specification.Free;
5+
6+
public class SSSTimerTaskCannotReschedule {
7+
8+
/*
9+
* Error cannot reschedule a timer
10+
*/
11+
public static void example1801324_simplified( @Borrowed Timer timer, String sessionKey, @Free TimerTask tt) {
12+
13+
// Step 2) Cancel the timer
14+
timer.cancel();
15+
16+
// Step 3 Schedule a new task for this timer -> ERROR Cannot reschedule a Timer
17+
timer.schedule(tt , 1000);
18+
}
19+
20+
}
21+
22+
/*
23+
* [If the timer is cancelled] any further attempt to schedule a task on the timer will result in an IllegalStateException
24+
*
25+
* START --- schedule() ----> [SCHEDULED]-------->
26+
* ----------------------------------------> cancel() -----> [CANCELLED] (no further scheduling allowed)
27+
*/
28+
class Timer{
29+
//@StateRefinement(this, to="cancelled")
30+
public void cancel() { }
31+
32+
// @StateRefinement(this, from="start", to="scheduled")
33+
public void schedule(TimerTask task, /* delay > 0 */int delay) {}
34+
35+
}
36+
37+
38+
// /*
39+
// * Error cannot reschedule a timer
40+
// */
41+
// public static void example1801324( Map<String, Timer> timers, String sessionKey) {
42+
43+
// // Step 1) Get the timer
44+
// Timer timer = timers.get(sessionKey);
45+
46+
// // Step 2) Cancel the timer
47+
// timer.cancel();
48+
49+
// // Step 3) Schedule a new task for this timer -> ERROR Cannot reschedule a Timer
50+
// timer.schedule(new TimerTask() {
51+
// @Override
52+
// public void run() {
53+
// System.out.println("Timer task completed.");
54+
// }
55+
// }, 1000);
56+
// }
57+
58+
59+

‎latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
import specification.Borrowed;
2+
import specification.Unique;
3+
4+
public class SSSURLConnectionReuseConnection {
5+
6+
public static void example4278917(@Borrowed URL address) {
7+
8+
try {
9+
// Step 1) Open the connection
10+
URLConnection connection = address.openConnection(); // returns a unique object
11+
12+
// Step 2) Connect
13+
connection.connect();
14+
15+
/* Other code in original question */
16+
17+
// Step 3) Setup parameters and connection properties after connection == ERROR
18+
connection.setAllowUserInteraction(true);
19+
connection.addRequestProperty("AUTHENTICATION_REQUEST_PROPERTY", "authorizationRequest");
20+
connection.getHeaderFields();
21+
22+
} catch (IOException e) {
23+
// Handle exceptions related to network or stream issues
24+
System.err.println("Error: " + e.getMessage());
25+
}
26+
}
27+
}
28+
29+
class URL{
30+
@Unique // @StateRefinement (return, to="manipulate")
31+
public URLConnection openConnection() {
32+
return new URLConnection();
33+
}
34+
}
35+
36+
37+
/**
38+
* --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT]
39+
* setAllowUserInteraction() getContent()
40+
* addRequestProperty()... getHeaderFields()...
41+
*/
42+
// @StateSet({"manipulate", "interact"})
43+
class URLConnection{
44+
45+
//@StateRefinement(this, from="manipulate")
46+
void setAllowUserInteraction(boolean b){}
47+
48+
//@StateRefinement(this, from="manipulate")
49+
void addRequestProperty(String s1, String s2){}
50+
51+
//@StateRefinement(this, from="interact")
52+
void getHeaderFields(){}
53+
54+
//@StateRefinement(this, from="manipulate", to="interact")
55+
void connect() throws IOException {}
56+
}
57+

‎latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
import specification.Borrowed;
2+
import specification.Unique;
3+
import java.io.IOException;
4+
import java.io.InputStream;
5+
6+
public class SSSURLConnectionSetProperty1 {
7+
8+
public static void example331538(@Borrowed URL address) {
9+
try {
10+
11+
// Step 1) Open the connection
12+
URLConnection cnx = address.openConnection();
13+
14+
// Step 2) Setup parameters and connection properties
15+
cnx.setAllowUserInteraction(false); // Step 2)
16+
cnx.setDoOutput(true);
17+
cnx.addRequestProperty("User-Agent", "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)");
18+
19+
20+
// Step 3)
21+
cnx.connect();
22+
23+
// Step 4)
24+
cnx.getContent();
25+
26+
// Get the input stream and process it
27+
InputStream is = cnx.getInputStream();
28+
System.out.println("Successfully opened input stream.");
29+
30+
// Ensure to close the InputStream after use
31+
is.close();
32+
33+
} catch (IOException e) {
34+
// Handle exceptions related to network or stream issues
35+
System.err.println("Error: " + e.getMessage());
36+
}
37+
}
38+
}
39+
40+
41+
42+
43+
class URL{
44+
@Unique // @StateRefinement (return, to="manipulate")
45+
public URLConnection openConnection() {
46+
return new URLConnection();
47+
}
48+
}
49+
50+
/**
51+
* --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT]
52+
* setAllowUserInteraction() getContent()
53+
* addRequestProperty()... getHeaderFields()...
54+
*/
55+
// @StateSet({"manipulate", "interact"})
56+
class URLConnection{
57+
58+
//@StateRefinement(this, from="manipulate")
59+
void setAllowUserInteraction(boolean b){}
60+
61+
//@StateRefinement(this, from="manipulate")
62+
void setDoOutput(boolean b){}
63+
64+
//@StateRefinement(this, from="manipulate")
65+
void addRequestProperty(String s1, String s2){}
66+
67+
//@StateRefinement(this, from="manipulate", to="interact")
68+
void connect() throws IOException {}
69+
70+
//@StateRefinement(this, from="interact")
71+
void getContent(){}
72+
73+
74+
//@StateRefinement(this, from="interact")
75+
@Unique //????? Not sure: Returns an input stream that reads from this open connection.
76+
InputStream getInputStream(){ return null;}
77+
78+
}

0 commit comments

Comments
 (0)