Skip to content

Commit 517d004

Browse files
rcosta358rcosta358
committed
BufferedReader Refinements
1 parent d93bd00 commit 517d004

File tree

6 files changed

+93
-99
lines changed

6 files changed

+93
-99
lines changed

‎examples/demo/src/main/java/com/bufferedreader/BufferedReaderRefinements.java‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
package com.bufferedreader;
2+
3+
import java.io.IOException;
4+
import java.io.Reader;
5+
import java.util.stream.Stream;
6+
7+
import liquidjava.specification.ExternalRefinementsFor;
8+
import liquidjava.specification.Refinement;
9+
import liquidjava.specification.RefinementAlias;
10+
import liquidjava.specification.StateRefinement;
11+
import liquidjava.specification.StateSet;
12+
13+
@RefinementAlias("NonNegative(int v) { v >= 0 }")
14+
@RefinementAlias("Positive(int v) { v > 0 }")
15+
@StateSet({"open", "marked", "closed"})
16+
@ExternalRefinementsFor("java.io.BufferedReader")
17+
public interface BufferedReaderRefinements {
18+
19+
@StateRefinement(to="open(this)")
20+
public void BufferedReader(Reader in);
21+
22+
@StateRefinement(to="open(this)")
23+
public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz);
24+
25+
@StateRefinement(from="open(this)", to="open(this)")
26+
@StateRefinement(from="marked(this)", to="marked(this)")
27+
public int read() throws IOException;
28+
29+
@StateRefinement(from="open(this)", to="open(this)")
30+
@StateRefinement(from="marked(this)", to="marked(this)")
31+
public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len) throws IOException; // cant write "|| len <= cbuf.length - off"
32+
33+
@StateRefinement(from="open(this)", to="open(this)")
34+
@StateRefinement(from="marked(this)", to="marked(this)")
35+
public String readLine() throws IOException;
36+
37+
@StateRefinement(from="open(this)", to="open(this)")
38+
@StateRefinement(from="marked(this)", to="marked(this)")
39+
public boolean ready() throws IOException;
40+
41+
@StateRefinement(from="open(this)", to="open(this)")
42+
@StateRefinement(from="marked(this)", to="marked(this)")
43+
public boolean markSupported();
44+
45+
@StateRefinement(from="open(this)", to="marked(this)")
46+
@StateRefinement(from="marked(this)", to="marked(this)")
47+
public void mark(@Refinement("NonNegative(_)") int readAheadLimit) throws IOException;
48+
49+
@StateRefinement(from="marked(this)", to="open(this)")
50+
public void reset() throws IOException;
51+
52+
@StateRefinement(from="!closed(this)", to="closed(this)")
53+
public void close() throws IOException;
54+
55+
@StateRefinement(from="open(this)", to="open(this)")
56+
@StateRefinement(from="marked(this)", to="marked(this)")
57+
public Stream<String> lines();
58+
}

‎examples/demo/src/main/java/com/bufferedreader/BufferedReaderTests.java‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
package com.bufferedreader;
2+
3+
import java.io.BufferedReader;
4+
import java.io.FileReader;
5+
6+
public class BufferedReaderTests {
7+
8+
void readClosedFile() throws Exception {
9+
BufferedReader in = new BufferedReader(new FileReader("foo.in"));
10+
in.close();
11+
in.read();
12+
}
13+
14+
void resetUnmarkedFile() throws Exception {
15+
BufferedReader in = new BufferedReader(new FileReader("foo.in"));
16+
in.reset();
17+
}
18+
19+
void negativeLength() throws Exception {
20+
BufferedReader in = new BufferedReader(new FileReader("foo.in"), -1);
21+
}
22+
23+
void noErrors() throws Exception {
24+
BufferedReader in = new BufferedReader(new FileReader("foo.in"), 100);
25+
int bufSize = 10;
26+
char[] buf = new char[bufSize];
27+
in.ready();
28+
in.read();
29+
in.readLine();
30+
in.mark(10);
31+
in.reset();
32+
in.read(buf, 0, bufSize);
33+
in.close();
34+
}
35+
}

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

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

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

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

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

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

‎examples/demo/src/test/java/com/example/AppTest.java‎

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

0 commit comments

Comments
 (0)