Skip to content

Commit a05507f

Browse files
rcosta358rcosta358
authored
Multiple Errors (#121)
1 parent 9b14c3f commit a05507f

40 files changed

+431
-649
lines changed

‎liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java‎

Lines changed: 10 additions & 96 deletions
Original file line numberDiff line numberDiff line change
@@ -4,102 +4,16 @@
44

55
class SimpleTest {
66

7-
@Refinement("return > 0")
8-
public int test() {
9-
return 10;
7+
void test1() {
8+
@Refinement("x > 0")
9+
int x = -1;
1010
}
11-
}
12-
13-
// @RefinementAlias("Percentage(int x) { 0 <= x && x <= 100 }")
14-
// @Refinement("Percentage(_)")
15-
// public static int addBonus(
16-
// @Refinement("Percentage(grade)") int grade,
17-
// @Refinement("Percentage(bonus) && (bonus < grade)")
18-
// int bonus) {
19-
//
20-
// if((grade + bonus) > 100)
21-
// return 100;
22-
//
23-
// else
24-
// return grade+bonus;
25-
// }
26-
//
27-
28-
// @Refinement("_ > 10")
29-
// int i = 10;
30-
31-
// @Refinement("sum(_) > 30")
32-
// Account a = new Account(50);
33-
// a.deposit(60);
34-
35-
// Account b = new Account(138);
36-
// b = a.transferTo(b, 10);
37-
//
38-
// @Refinement("sum(_) == 148")
39-
// Account c = b;
40-
41-
// Order o = new Order();
42-
//
43-
// Order f = o.addItem("shirt", 60).addGift();
44-
// .getNewOrderPayThis().addItem("t", 6).addItem("t", 1);
45-
// o.addGift();
46-
// f.addItem("l", 1).pay(000).addGift().pay(000);//.addTransportCosts().sendToAddress("home");
47-
48-
// TrafficLight tl = new TrafficLight();
49-
// tl.transitionToAmber();
50-
//
51-
52-
// TrafficLight tl2 = tl.getTrafficLightStartingRed();
53-
// tl2.transitionToFlashingAmber();
54-
55-
// tl.transitionToAmber();
56-
// tl.transitionToAmber();
57-
58-
// tl.passagersCross();
59-
// tl.intermitentMalfunction();
6011

61-
// tl.transitionToFlashingAmber();
12+
void test2() {
13+
@Refinement("y > 0")
14+
int y = -2;
6215

63-
// @Refinement("size(al) < 4")
64-
// ArrayList<Integer> al = new ArrayList<Integer>();
65-
// al.add(1);
66-
// al.add(1);
67-
// al.get(2);
68-
69-
// @Refinement("size(t) == 3")
70-
// ArrayList<Integer> t = al;
71-
72-
//
73-
// Order o = new Order();
74-
// o.addItem("shirt", 5)
75-
// .addItem("shirt", 10)
76-
// .addItem("h", 20)
77-
// .addItem("h", 6);
78-
79-
// InputStreamReader isr = new InputStreamReader(System.in);
80-
// isr.read();
81-
// isr.read();
82-
// isr.read();
83-
// isr.close();
84-
//
85-
// //...
86-
// isr.read();
87-
88-
// @Refinement("_ > 0")
89-
// public int fun (int[] arr) {
90-
// return max(arr[0], 1);
91-
// }
92-
//
93-
94-
// //@Refinement("_.length(x) >= 0") ==
95-
//// @Refinement("length(_, x) >= 0")
96-
//// int[] a1 = new int[5];
97-
// K(.., ..)
98-
99-
// }
100-
101-
// See error NaN
102-
// @Refinement("true")
103-
// double b = 0/0;
104-
// @Refinement("_ > 5")
105-
// double c = b;
16+
@Refinement("z > 0")
17+
int z = 3;
18+
}
19+
}

‎liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package testMultiple;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
class MultipleErrorsExample {
6+
7+
void test1() {
8+
@Refinement("a > 0")
9+
int a = -1;
10+
}
11+
12+
void test2() {
13+
@Refinement("b > 0")
14+
int b = -2;
15+
16+
@Refinement("c > 0")
17+
int c = -3;
18+
}
19+
}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/CustomError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.StateSet;
44

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.Ghost;
44
import liquidjava.specification.StateRefinement;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.StateRefinement;
44
import liquidjava.specification.StateSet;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.Refinement;
44

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.Refinement;
44

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.Refinement;
44

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.StateRefinement;
44
import liquidjava.specification.StateSet;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java renamed to liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
package testingInProgress.diagnostics.errors;
1+
package testMultiple.errors;
22

33
import liquidjava.specification.StateRefinement;
44
import liquidjava.specification.StateSet;

0 commit comments

Comments
 (0)