Skip to content

Add examples #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 4 commits into from
Apr 15, 2025
Merged

Add examples #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2df34cc
add example for urlconnection reuse
CatarinaGamboa Feb 12, 2025
d9a15b3
add examples urlconnection property with several methods
CatarinaGamboa Feb 12, 2025
8959494
add example for timertask
CatarinaGamboa Feb 12, 2025
78225c3
add examples
CatarinaGamboa Apr 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
213 changes: 43 additions & 170 deletions latte-umbrella/src/main/java/examples/MyStackTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,186 +1,59 @@
package examples;

import java.io.BufferedReader;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.ArrayList;

import specification.Borrowed;
import specification.Free;
import specification.Shared;
import specification.Unique;
public class MyStackTest {

import java.io.UnsupportedEncodingException;
public static void main(String[] args) {

public class MyStackTest {
}
// Define and initialize queues
LinkedList<Integer> 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);

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()
// Get an iterator for the queue
Iterator<Integer> iterator = qev1.iterator();

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

class HttpResponse {
// TODO: STUB METHOD
public HttpEntity getEntity() {
return new HttpEntity();
}

}

class HttpEntity {
// TODO: STUB METHOD
public InputStream getContent() {
return (InputStream) new Object();
}
// @ExternalRefinementsFor("java.util.Iterator")
// @StateSet({"start", "ready", "inNext"})
class Iterator<N> {

// @StateRefinement(to = "start(this)")
public Iterator(){}

// @StateRefinement(to = "ready(this)")
public boolean hasNext(){return true;}

// @StateRefinement(from = "ready(this)", to = "inNext(this)")
public Object next(){return null;}

// @StateRefinement(from = "inNext(this)", to = "start(this)")
public void remove(){}
}

// @ExternalRefinementsFor("java.util.LinkedList")
class LinkedList<T> {

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

// class Box {
// @Unique int value;
// void add(@Owned int delta) {
// // ERROR: RHS and LHS are not separately unique
// this.value = this.value + this.delta;
// }
// void test() {
// int x = 123;
// Box b1 = new Box(x);
// // ERROR: ‘x‘ is consumed since ‘value‘ is unique,
// // thus it is unaccessible
// Box b2 = new Box(x);
// }
// void makeBox2() {
// // ERROR: ‘this.value‘ is unique, thus cannot be
// // passed to a shared parameter
// return new Box2(this.value);
// }
// }
// class Box2 { @Shared int value; }



// HttpResponse response = r;
// InputStream in = response.getEntity().getContent();
// BufferedReader reader = new BufferedReader(
// new InputStreamReader(
// response.getEntity().getContent(), "UTF-8")); // Second call to getEntity()



// @Unique Node root;

// public MyStack(@Free Node root) {
// this.root = root;
// }


// void push( @Free Object value) {
// Node r;
// Node n;

// r = this.root; // save root in r
// this.root = null; //nullify root
// n = new Node(value, r); //create new root
// this.root = n; //replace root
// }


// @Free Object pop (){
// Object value;

// if (this.root == null) {
// value = null;
// } else {
// Node r = root;
// value = r.value;
// Node n;
// n = r.next;
// r.next = null;
// r.value = null;
// this.root = n;
// }
// return value;
// }

// // public @Unique Object dequeue() {
// // Node r = this.root;
// // //r : alias(this.root)
// // if (r == null || r.next == null) {
// // // In an empty or single-element stack, dequeue and pop
// // // are equivalent
// // return pop();
// // } else {

// // // `this` and `this.root` are effectively alias, thus
// // // we cannot pass `this.root` to `this.dequeue` without
// // // doing a destructive read
// // this.root = null;
// // // r : unique

// // Object value = dequeueHelper(r);
// // // value : unique

// // // Since `dequeue` only detaches the next node of the one
// // // passed to it, it will never need to detach `root`, so
// // // we can just restore it back to the original value.
// // this.root = r;
// // // r : alias(this.root)

// // return value;
// // }
// // }

// // private @Free Object dequeueHelper(@Borrowed Node n) {
// // // Look ahead two steps so that we can disconnect the *next*
// // // node by mutating the node that will remain in the stack.

// // Node nn = n.next;
// // // nn : alias(n.next)

// // if (nn.next == null) {
// // n.next = null;
// // // nn : unique

// // Object value = nn.value;
// // // value : alias(nn.value)

// // nn.value = null;
// // // value : unique

// // return value;
// // } else {
// // return dequeueHelper(n.next);
// // }
// // }
// }

// /**
// * Node class for the stack example
// * Uses @Unique annotations to specify that the value and next fields are unique
// * in the scope of the Node class
// * @author catarina gamboa
// *
// */
// class Node {

// @Unique Object value;
// @Unique Node next;

// /**
// * Constructor for the Node class using @Free value and next nodes
// * @param value
// * @param next
// */
// public Node (@Free Object value, @Free Node next) {
// this.value = value;
// this.next = next;
// }
// }
public void add(T t){}
}
0 ...c/test/examples/ResultSetForwardOnly.java → ...ing_state_space/ResultSetForwardOnly.java
View file
Open in desktop
File renamed without changes.
10 changes: 5 additions & 5 deletions ...la/src/test/examples/ResultSetNoNext.java → ...earching_state_space/ResultSetNoNext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
import specification.Free;
import specification.Unique;

public class ResultSetNoNext {
public class SSSResultSetNoNext {


/*
Expand Down Expand Up @@ -42,19 +42,19 @@ public PreparedStatement prepareStatement(String s) {
// prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){}
}


class PreparedStatement{
void setString(int index, String s){}

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

//@StateSet({"beforeRow", "onRow"})
class ResultSet{
// @StateRefinement(this, col > 0)
// @StateRefinement( from = "onRow")
float getFloat(String s){return 0;}

// @StateRefinement(this, col == old(col) + 1)
// @StateRefinement( to="onRow")
void next(){}
}

Expand Down
14 changes: 7 additions & 7 deletions ...t/examples/TimerTaskCannotReschedule.java → ...tate_space/TimerTaskCannotReschedule.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
import specification.Borrowed;
import specification.Free;

public class TimerTaskCannotReschedule {
public class SSSTimerTaskCannotReschedule {

/*
* Error cannot reschedule a timer
Expand Down Expand Up @@ -47,12 +47,12 @@ public void schedule(TimerTask task, /* delay > 0 */int delay) {}
// 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);
// timer.schedule(new TimerTask() {
// @Override
// public void run() {
// System.out.println("Timer task completed.");
// }
// }, 1000);
// }


Expand Down
2 changes: 1 addition & 1 deletion ...xamples/URLConnectionReuseConnection.java → ...e_space/URLConnectionReuseConnection.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import specification.Borrowed;
import specification.Unique;

public class URLConnectionReuseConnection {
public class SSSURLConnectionReuseConnection {

public static void example4278917(@Borrowed URL address) {

Expand Down
5 changes: 2 additions & 3 deletions ...t/examples/URLConnectionSetProperty1.java → ...tate_space/URLConnectionSetProperty1.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
import java.io.IOException;
import java.io.InputStream;

public class URLConnectionSetProperty1 {
public class SSSURLConnectionSetProperty1 {

public static void example331538(@Borrowed URL address) {
try {
Expand All @@ -14,8 +14,7 @@ public static void example331538(@Borrowed URL address) {
// 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)");
cnx.addRequestProperty("User-Agent", "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)");


// Step 3)
Expand Down
2 changes: 1 addition & 1 deletion ...onnectionSetPropertyMultipleComplete.java → ...onnectionSetPropertyMultipleComplete.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
import specification.Shared;
import specification.Unique;

public class URLConnectionSetPropertyMultipleComplete {
public class SSSURLConnectionSetPropertyMultipleComplete {

String sessionId = "1234";
public void example5368535(@Borrowed URL address, String content) {
Expand Down
2 changes: 1 addition & 1 deletion ...RLConnectionSetPropertyMultipleShort.java → ...RLConnectionSetPropertyMultipleShort.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
import specification.Shared;
import specification.Unique;

public class URLConnectionSetPropertyMultipleShort {
public class SSSURLConnectionSetPropertyMultipleShort {

String sessionId = "1234";
public void example5368535(@Borrowed URL address, String content) {
Expand Down
5 changes: 5 additions & 0 deletions latte-umbrella/src/test/examples/stack_overflow/Iterator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
public class Iterator {



}
Loading