Skip to content

Commit 023c8d7

Browse files
alcidesalcides
committed
Barista example
1 parent 26cec5b commit 023c8d7

5 files changed

Lines changed: 126 additions & 1 deletion

File tree

‎examples/demo/src/main/java/com/example/awt/PopupMenu.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package com.example.awt;
2+
3+
import java.awt.Component;
4+
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
import liquidjava.specification.Ghost;
7+
import liquidjava.specification.Refinement;
8+
9+
10+
11+
@ExternalRefinementsFor("java.awt.PopupMenu")
12+
@Ghost("boolean isShowing")
13+
public interface PopupMenu {
14+
15+
/* Should also include hierarchy, but we do not support sets. */
16+
public void show(@Refinement("isShowing(origin) && isShowing(this)") Component origin, int x, int y);
17+
18+
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
package com.example.simple;
2+
23
import liquidjava.specification.Refinement;
34

45
public class SimpleExample {

‎examples/demo/src/main/java/com/example/xml/TransformerException.java‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
package com.example.xml;
2+
3+
import javax.xml.transform.SourceLocator;
4+
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
import liquidjava.specification.StateRefinement;
7+
import liquidjava.specification.StateSet;
8+
9+
10+
/*
11+
State machine:
12+
13+
withCause (Constructors with throwable)
14+
15+
^ initCause
16+
17+
withoutCause (other constructors)
18+
19+
*/
20+
21+
@ExternalRefinementsFor("javax.xml.transform.TransformerException")
22+
@StateSet({"withoutCause", "withCause"})
23+
public interface TransformerException {
24+
25+
@StateRefinement(to="withoutCause(this)")
26+
public void TransformerException(String msg);
27+
28+
@StateRefinement(to="withoutCause(this)")
29+
public void TransformerException(String msg, SourceLocator locator);
30+
31+
@StateRefinement(to="withCause(this)")
32+
public void TransformerException(Throwable cause);
33+
34+
@StateRefinement(to="withCause(this)")
35+
public void TransformerException(String message, Throwable cause);
36+
37+
@StateRefinement(to="withCause(this)")
38+
public void TransformerException(String message, SourceLocator locator, Throwable cause);
39+
40+
@StateRefinement(from="withoutCause(this)", to="withCause(this)")
41+
public Throwable initCause(Throwable cause);
42+
43+
// This would be useful if we wanted to get rid of nulls.
44+
// Same for location
45+
//@StateRefinement(from="withCause(this)")
46+
public Throwable getCause();
47+
}

‎examples/demo/src/main/java/com/example/zip/ZipFile.java‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
package com.example.zip;
2+
3+
import java.io.File;
4+
import java.io.InputStream;
5+
import java.nio.charset.Charset;
6+
import java.util.Enumeration;
7+
import java.util.zip.ZipEntry;
8+
9+
import liquidjava.specification.ExternalRefinementsFor;
10+
import liquidjava.specification.StateRefinement;
11+
import liquidjava.specification.StateSet;
12+
13+
14+
/*
15+
State machine:
16+
17+
closed
18+
19+
^ close
20+
21+
opened. @ getEntry, getIS, stream, entries
22+
23+
*/
24+
25+
@ExternalRefinementsFor("java.util.zip.ZipFile")
26+
@StateSet({"opened", "closed"})
27+
public interface ZipFile {
28+
29+
@StateRefinement(to="opened(this)")
30+
public void ZipFile(File file);
31+
32+
@StateRefinement(to="opened(this)")
33+
public void ZipFile(File file, int mode);
34+
35+
@StateRefinement(to="opened(this)")
36+
public void ZipFile(File file, int mode, Charset cs);
37+
38+
@StateRefinement(to="opened(this)")
39+
public void ZipFile(File file, Charset cs);
40+
41+
@StateRefinement(to="opened(this)")
42+
public void ZipFile(String name);
43+
44+
@StateRefinement(to="opened(this)")
45+
public void ZipFile(String name, Charset cs);
46+
47+
@StateRefinement(from="opened(this)", to="closed(this)")
48+
public void close();
49+
50+
@StateRefinement(from="opened(this)")
51+
public Enumeration<? extends ZipEntry> entries();
52+
53+
@StateRefinement(from="opened(this)")
54+
public ZipEntry getEntry(String name);
55+
56+
@StateRefinement(from="opened(this)")
57+
public InputStream getInputStream(ZipEntry e);
58+
59+
60+
}

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
package com.example;
22

33
import static org.junit.Assert.assertTrue;
4-
54
import org.junit.Test;
65

76
/**

0 commit comments

Comments
 (0)