Skip to content

Commit d28327c

Browse files
CatarinaGamboaCatarinaGamboa
authored
Add examples (#2)
## Description Add examples that we want to support ## Example Multiple examples ## Type of change - [x] Examples - [ ] Bug fix - [ ] New feature - [ ] Documentation update - [ ] Code refactoring
1 parent 2d3aa3e commit d28327c

11 files changed

Lines changed: 152 additions & 195 deletions

File tree

‎latte-umbrella/src/main/java/examples/MyStackTest.java‎

Lines changed: 43 additions & 170 deletions
Original file line numberDiff line numberDiff line change
@@ -1,186 +1,59 @@
11
package examples;
22

3-
import java.io.BufferedReader;
4-
import java.io.InputStream;
5-
import java.io.InputStreamReader;
6-
import java.util.ArrayList;
73

8-
import specification.Borrowed;
9-
import specification.Free;
10-
import specification.Shared;
11-
import specification.Unique;
4+
public class MyStackTest {
125

13-
import java.io.UnsupportedEncodingException;
6+
public static void main(String[] args) {
147

15-
public class MyStackTest {
16-
}
8+
// Define and initialize queues
9+
LinkedList<Integer> qev1, qev2, qcv1, qcv2;
10+
qev1 = new LinkedList<>();
11+
qev2 = new LinkedList<>();
12+
qcv1 = new LinkedList<>();
13+
qcv2 = new LinkedList<>();
1714

15+
qev1.add(100);
16+
qev1.add(200);
17+
qev1.add(300);
18+
qev1.add(300);
19+
qev1.add(300);
20+
qev1.add(300);
1821

19-
class Test {
20-
public static void test(HttpResponse r) throws UnsupportedEncodingException {
21-
HttpResponse response = r;
22-
InputStream in = response.getEntity().getContent();
23-
BufferedReader reader = new BufferedReader(
24-
new InputStreamReader(
25-
response.getEntity().getContent(), "UTF-8")); // Second call to getEntity()
22+
// Get an iterator for the queue
23+
Iterator<Integer> iterator = qev1.iterator();
2624

27-
//Cannot call getContent twice if the entity is not repeatable. There is a method isRepeatable() to check
28-
}
29-
}
25+
try {
26+
iterator.remove(); // Error no call to next before remove
27+
}
28+
catch(UnsupportedOperationException e) {
29+
System.out.println("Calling Iterator.remove() and throwing exception.");
30+
}
3031

31-
class HttpResponse {
32-
// TODO: STUB METHOD
33-
public HttpEntity getEntity() {
34-
return new HttpEntity();
3532
}
33+
3634
}
3735

38-
class HttpEntity {
39-
// TODO: STUB METHOD
40-
public InputStream getContent() {
41-
return (InputStream) new Object();
42-
}
36+
// @ExternalRefinementsFor("java.util.Iterator")
37+
// @StateSet({"start", "ready", "inNext"})
38+
class Iterator<N> {
39+
40+
// @StateRefinement(to = "start(this)")
41+
public Iterator(){}
42+
43+
// @StateRefinement(to = "ready(this)")
44+
public boolean hasNext(){return true;}
45+
46+
// @StateRefinement(from = "ready(this)", to = "inNext(this)")
47+
public Object next(){return null;}
48+
49+
// @StateRefinement(from = "inNext(this)", to = "start(this)")
50+
public void remove(){}
4351
}
4452

53+
// @ExternalRefinementsFor("java.util.LinkedList")
54+
class LinkedList<T> {
4555

56+
public Iterator<T> iterator(){return null;}
4657

47-
// class Box {
48-
// @Unique int value;
49-
// void add(@Owned int delta) {
50-
// // ERROR: RHS and LHS are not separately unique
51-
// this.value = this.value + this.delta;
52-
// }
53-
// void test() {
54-
// int x = 123;
55-
// Box b1 = new Box(x);
56-
// // ERROR: ‘x‘ is consumed since ‘value‘ is unique,
57-
// // thus it is unaccessible
58-
// Box b2 = new Box(x);
59-
// }
60-
// void makeBox2() {
61-
// // ERROR: ‘this.value‘ is unique, thus cannot be
62-
// // passed to a shared parameter
63-
// return new Box2(this.value);
64-
// }
65-
// }
66-
// class Box2 { @Shared int value; }
67-
68-
69-
70-
// HttpResponse response = r;
71-
// InputStream in = response.getEntity().getContent();
72-
// BufferedReader reader = new BufferedReader(
73-
// new InputStreamReader(
74-
// response.getEntity().getContent(), "UTF-8")); // Second call to getEntity()
75-
76-
77-
78-
// @Unique Node root;
79-
80-
// public MyStack(@Free Node root) {
81-
// this.root = root;
82-
// }
83-
84-
85-
// void push( @Free Object value) {
86-
// Node r;
87-
// Node n;
88-
89-
// r = this.root; // save root in r
90-
// this.root = null; //nullify root
91-
// n = new Node(value, r); //create new root
92-
// this.root = n; //replace root
93-
// }
94-
95-
96-
// @Free Object pop (){
97-
// Object value;
98-
99-
// if (this.root == null) {
100-
// value = null;
101-
// } else {
102-
// Node r = root;
103-
// value = r.value;
104-
// Node n;
105-
// n = r.next;
106-
// r.next = null;
107-
// r.value = null;
108-
// this.root = n;
109-
// }
110-
// return value;
111-
// }
112-
113-
// // public @Unique Object dequeue() {
114-
// // Node r = this.root;
115-
// // //r : alias(this.root)
116-
// // if (r == null || r.next == null) {
117-
// // // In an empty or single-element stack, dequeue and pop
118-
// // // are equivalent
119-
// // return pop();
120-
// // } else {
121-
122-
// // // `this` and `this.root` are effectively alias, thus
123-
// // // we cannot pass `this.root` to `this.dequeue` without
124-
// // // doing a destructive read
125-
// // this.root = null;
126-
// // // r : unique
127-
128-
// // Object value = dequeueHelper(r);
129-
// // // value : unique
130-
131-
// // // Since `dequeue` only detaches the next node of the one
132-
// // // passed to it, it will never need to detach `root`, so
133-
// // // we can just restore it back to the original value.
134-
// // this.root = r;
135-
// // // r : alias(this.root)
136-
137-
// // return value;
138-
// // }
139-
// // }
140-
141-
// // private @Free Object dequeueHelper(@Borrowed Node n) {
142-
// // // Look ahead two steps so that we can disconnect the *next*
143-
// // // node by mutating the node that will remain in the stack.
144-
145-
// // Node nn = n.next;
146-
// // // nn : alias(n.next)
147-
148-
// // if (nn.next == null) {
149-
// // n.next = null;
150-
// // // nn : unique
151-
152-
// // Object value = nn.value;
153-
// // // value : alias(nn.value)
154-
155-
// // nn.value = null;
156-
// // // value : unique
157-
158-
// // return value;
159-
// // } else {
160-
// // return dequeueHelper(n.next);
161-
// // }
162-
// // }
163-
// }
164-
165-
// /**
166-
// * Node class for the stack example
167-
// * Uses @Unique annotations to specify that the value and next fields are unique
168-
// * in the scope of the Node class
169-
// * @author catarina gamboa
170-
// *
171-
// */
172-
// class Node {
173-
174-
// @Unique Object value;
175-
// @Unique Node next;
176-
177-
// /**
178-
// * Constructor for the Node class using @Free value and next nodes
179-
// * @param value
180-
// * @param next
181-
// */
182-
// public Node (@Free Object value, @Free Node next) {
183-
// this.value = value;
184-
// this.next = next;
185-
// }
186-
// }
58+
public void add(T t){}
59+
}

latte-umbrella/src/test/examples/ResultSetForwardOnly.java renamed to latte-umbrella/src/test/examples/searching_state_space/ResultSetForwardOnly.java

File renamed without changes.

latte-umbrella/src/test/examples/ResultSetNoNext.java renamed to latte-umbrella/src/test/examples/searching_state_space/ResultSetNoNext.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
import specification.Free;
66
import specification.Unique;
77

8-
public class ResultSetNoNext {
8+
public class SSSResultSetNoNext {
99

1010

1111
/*
@@ -42,19 +42,19 @@ public PreparedStatement prepareStatement(String s) {
4242
// prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){}
4343
}
4444

45-
4645
class PreparedStatement{
4746
void setString(int index, String s){}
4847

49-
// @StateRefinement(return, to="TYPE_FORWARD_ONLY, col == -1")
48+
// @ReturnState( to="TYPE_FORWARD_ONLY, beforeRow")
5049
ResultSet executeQuery(String s){return null;}
5150
}
5251

52+
//@StateSet({"beforeRow", "onRow"})
5353
class ResultSet{
54-
// @StateRefinement(this, col > 0)
54+
// @StateRefinement( from = "onRow")
5555
float getFloat(String s){return 0;}
5656

57-
// @StateRefinement(this, col == old(col) + 1)
57+
// @StateRefinement( to="onRow")
5858
void next(){}
5959
}
6060

latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java renamed to latte-umbrella/src/test/examples/searching_state_space/TimerTaskCannotReschedule.java

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import specification.Borrowed;
44
import specification.Free;
55

6-
public class TimerTaskCannotReschedule {
6+
public class SSSTimerTaskCannotReschedule {
77

88
/*
99
* Error cannot reschedule a timer
@@ -47,12 +47,12 @@ public void schedule(TimerTask task, /* delay > 0 */int delay) {}
4747
// timer.cancel();
4848

4949
// // 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);
50+
// timer.schedule(new TimerTask() {
51+
// @Override
52+
// public void run() {
53+
// System.out.println("Timer task completed.");
54+
// }
55+
// }, 1000);
5656
// }
5757

5858

latte-umbrella/src/test/examples/URLConnectionReuseConnection.java renamed to latte-umbrella/src/test/examples/searching_state_space/URLConnectionReuseConnection.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import specification.Borrowed;
22
import specification.Unique;
33

4-
public class URLConnectionReuseConnection {
4+
public class SSSURLConnectionReuseConnection {
55

66
public static void example4278917(@Borrowed URL address) {
77

latte-umbrella/src/test/examples/URLConnectionSetProperty1.java renamed to latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetProperty1.java

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import java.io.IOException;
44
import java.io.InputStream;
55

6-
public class URLConnectionSetProperty1 {
6+
public class SSSURLConnectionSetProperty1 {
77

88
public static void example331538(@Borrowed URL address) {
99
try {
@@ -14,8 +14,7 @@ public static void example331538(@Borrowed URL address) {
1414
// Step 2) Setup parameters and connection properties
1515
cnx.setAllowUserInteraction(false); // Step 2)
1616
cnx.setDoOutput(true);
17-
cnx.addRequestProperty("User-Agent",
18-
"Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)");
17+
cnx.addRequestProperty("User-Agent", "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)");
1918

2019

2120
// Step 3)

latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java renamed to latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleComplete.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
import specification.Shared;
77
import specification.Unique;
88

9-
public class URLConnectionSetPropertyMultipleComplete {
9+
public class SSSURLConnectionSetPropertyMultipleComplete {
1010

1111
String sessionId = "1234";
1212
public void example5368535(@Borrowed URL address, String content) {

latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java renamed to latte-umbrella/src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
import specification.Shared;
77
import specification.Unique;
88

9-
public class URLConnectionSetPropertyMultipleShort {
9+
public class SSSURLConnectionSetPropertyMultipleShort {
1010

1111
String sessionId = "1234";
1212
public void example5368535(@Borrowed URL address, String content) {

‎latte-umbrella/src/test/examples/stack_overflow/Iterator.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
public class Iterator {
2+
3+
4+
5+
}

0 commit comments

Comments
 (0)