Skip to content

Commit 26cec5b

Browse files
rcosta358rcosta358
authored
Update Examples
2 parents d93bd00 + 08e65d3 commit 26cec5b

File tree

10 files changed

+128
-36
lines changed

10 files changed

+128
-36
lines changed

‎examples/demo/src/main/java/com/example/TestSimple.java‎

Lines changed: 0 additions & 17 deletions
This file was deleted.

examples/demo/src/main/java/com/example/TestArrayDeque.java renamed to examples/demo/src/main/java/com/example/arraydeque/ArrayDequeExample.java

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,19 @@
1-
package com.example;
1+
package com.example.arraydeque;
22

3-
import java.io.IOException;
43
import java.util.ArrayDeque;
54

6-
public class TestArrayDeque {
5+
public class ArrayDequeExample {
76

8-
public static void main(String[] args) throws IOException{
9-
/*Uncomment Below*/
7+
public static void main(String[] args) {
108
ArrayDeque<Integer> p = new ArrayDeque<>();
119
p.add(2);
1210
p.remove();
1311
p.offerFirst(6);
1412
p.getLast();
1513
p.remove();
16-
// p.getLast();
14+
// p.getLast(); // uncomment for error
1715
p.add(78);
1816
p.add(8);
1917
p.getFirst();
20-
21-
2218
}
23-
2419
}

examples/demo/src/main/java/com/example/ArrayDequeRefinements.java renamed to examples/demo/src/main/java/com/example/arraydeque/ArrayDequeRefinements.java

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package com.example;
1+
package com.example.arraydeque;
22

33
import liquidjava.specification.ExternalRefinementsFor;
44
import liquidjava.specification.Ghost;
@@ -11,28 +11,27 @@ public interface ArrayDequeRefinements<E> {
1111

1212
public void ArrayDeque();
1313

14-
@StateRefinement(to="size(this) == (size(old(this)) + 1)")
14+
@StateRefinement(to="size(this) == size(old(this)) + 1")
1515
public boolean add(E elem);
1616

17-
@StateRefinement(to="size(this) == (size(old(this)) + 1)")
17+
@StateRefinement(to="size(this) == size(old(this)) + 1")
1818
public boolean offerFirst(E elem);
1919

20-
@StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))")
20+
@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this))")
2121
public E getFirst();
2222

23-
@StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))")
23+
@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this))")
2424
public E getLast();
2525

26-
@StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)")
27-
public void remove();
26+
@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1")
27+
public E remove();
2828

29-
@StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)")
29+
@StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1")
3030
public E pop();
3131

3232
@Refinement("_ == size(this)")
3333
public int size();
3434

35-
@Refinement("_ == (size(this) <= 0)")
35+
@Refinement("_ == size(this) <= 0")
3636
public boolean isEmpty();
37-
3837
}

‎examples/demo/src/main/java/com/example/arraylist/ArrayListExample.java‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package com.example.arraylist;
2+
3+
import java.util.ArrayList;
4+
5+
public class ArrayListExample {
6+
7+
public static void main(String[] args) {
8+
ArrayList<String> list = new ArrayList<>();
9+
list.add("a");
10+
// list.get(1); // uncomment for error
11+
}
12+
}

‎examples/demo/src/main/java/com/example/arraylist/ArrayListRefinements.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package com.example.arraylist;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.Ghost;
5+
import liquidjava.specification.Refinement;
6+
import liquidjava.specification.StateRefinement;
7+
8+
@ExternalRefinementsFor("java.util.ArrayList")
9+
@Ghost("int size")
10+
public interface ArrayListRefinements<E> {
11+
12+
@StateRefinement(to="size(this) == 0")
13+
public void ArrayList();
14+
15+
@StateRefinement(to="size(this) == size(old(this)) + 1")
16+
public boolean add(E elem);
17+
18+
public E get(@Refinement("0 <= _ && _ < size(this)") int index);
19+
}

‎examples/demo/src/main/java/com/example/reentrantlock/ReentrantLockExample.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package com.example.reentrantlock;
2+
3+
import java.util.concurrent.locks.ReentrantLock;
4+
5+
public class ReentrantLockExample {
6+
7+
public static void main(String[] args) {
8+
ReentrantLock lock = new ReentrantLock();
9+
lock.lock();
10+
lock.unlock();
11+
// lock.unlock(); // uncomment for error
12+
}
13+
}

‎examples/demo/src/main/java/com/example/reentrantlock/ReentrantLockRefinements.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package com.example.reentrantlock;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.util.concurrent.locks.ReentrantLock")
8+
@StateSet({"unlocked", "locked"})
9+
public interface ReentrantLockRefinements {
10+
11+
@StateRefinement(to="unlocked(this)")
12+
public void ReentrantLock();
13+
14+
@StateRefinement(from="unlocked(this)", to="locked(this)")
15+
public void lock();
16+
17+
@StateRefinement(from="locked(this)", to="unlocked(this)")
18+
public void unlock();
19+
}

‎examples/demo/src/main/java/com/example/simple/SimpleExample.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package com.example.simple;
2+
import liquidjava.specification.Refinement;
3+
4+
public class SimpleExample {
5+
6+
public static void main( String[] args ) {
7+
int a = 6;
8+
int b = 3;
9+
10+
@Refinement("x > 0")
11+
int x = -(a / b);
12+
}
13+
}

‎examples/demo/src/main/java/com/example/socket/SocketExample.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package com.example.socket;
2+
3+
import java.net.*;
4+
5+
public class SocketExample {
6+
7+
public static void main(String[] args) throws Exception {
8+
Socket socket = new Socket();
9+
socket.bind(new InetSocketAddress("localhost", 8080)); // comment for error
10+
socket.connect(new InetSocketAddress("example.com", 80));
11+
socket.close();
12+
}
13+
}

‎examples/demo/src/main/java/com/example/socket/SocketRefinements.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
package com.example.socket;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
import java.net.SocketAddress;
7+
8+
@ExternalRefinementsFor("java.net.Socket")
9+
@StateSet({"unconnected", "bound", "connected", "closed"})
10+
public interface SocketRefinements {
11+
12+
@StateRefinement(to="unconnected(this)")
13+
public void Socket();
14+
15+
@StateRefinement(from="unconnected(this)", to="bound(this)")
16+
public void bind(SocketAddress add);
17+
18+
@StateRefinement(from="bound(this)", to="connected(this)")
19+
public void connect(SocketAddress add);
20+
21+
@StateRefinement(from="connected(this)")
22+
public void sendUrgentData(int n);
23+
24+
@StateRefinement(from="!closed(this)", to="closed(this)")
25+
public void close();
26+
}

0 commit comments

Comments
 (0)