Skip to content

Commit 3fb2ed9

Browse files
committed
Several Improvements
1 parent 1f6b458 commit 3fb2ed9

20 files changed

+153
-161
lines changed

README.md

Lines changed: 25 additions & 18 deletions
Large diffs are not rendered by default.

src/main/java/com/tutorial/part1/ExampleRefinements.java

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

src/main/java/com/tutorial/part1/ExampleMethodRefinements.java renamed to src/main/java/com/tutorial/part1/MethodRefinementExample.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
import liquidjava.specification.Refinement;
44

5-
public class ExampleMethodRefinements {
5+
public class MethodRefinementExample {
66

77
public static int divide(int a, @Refinement("b != 0") int b) {
88
return a / b;
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package com.tutorial.part1;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class RefinementsExample {
7+
8+
public static void main(String[] args) {
9+
// @Refinement("positive > 0")
10+
int positive = -1;
11+
12+
// @Refinement("nonzero != 0")
13+
int nonzero = 0;
14+
15+
// @Refinement("0 <= _ && _ <= 100")
16+
int percentage = 200;
17+
}
18+
}

src/main/java/com/tutorial/part1/exercise/ExampleBankRefinements.java renamed to src/main/java/com/tutorial/part1/exercise/Bank.java

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
import liquidjava.specification.Refinement;
44

5-
public class ExampleBankRefinements {
5+
public class Bank {
66

77
@Refinement("true")
88
public static int deposit(@Refinement("true") int balance, @Refinement("true") int amount) {
@@ -13,11 +13,4 @@ public static int deposit(@Refinement("true") int balance, @Refinement("true") i
1313
public static int withdraw(@Refinement("true") int balance, @Refinement("true") int amount) {
1414
return balance - amount;
1515
}
16-
17-
public static void main(String[] args) {
18-
int balance = 0;
19-
balance = deposit(balance, 10);
20-
balance = withdraw(balance, 20); // should be an error
21-
System.out.println(balance);
22-
}
23-
}
16+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
package com.tutorial.part1.exercise;
2+
3+
public class BankExample {
4+
5+
public static void main(String[] args) {;
6+
int b = 0;
7+
b = Bank.deposit(b, 10);
8+
b = Bank.withdraw(b, 20); // should be an error
9+
System.out.println(b);
10+
}
11+
}

src/main/java/com/tutorial/part2/ExampleStateRefinements.java

Lines changed: 0 additions & 24 deletions
This file was deleted.
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
package com.tutorial.part2;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
@StateSet({"on", "off"})
7+
public class LightBulb {
8+
9+
@StateRefinement(to="off(this)")
10+
public LightBulb() {}
11+
12+
@StateRefinement(from="off(this)", to="on(this)")
13+
public void turnOn() {}
14+
15+
@StateRefinement(from="on(this)", to="off(this)")
16+
public void turnOff() {}
17+
18+
public static void main(String[] args) {
19+
LightBulb bulb = new LightBulb();
20+
bulb.turnOn();
21+
bulb.turnOff();
22+
// bulb.turnOff(); // uncomment for error
23+
}
24+
}

src/main/java/com/tutorial/part2/exercise/ExampleFileUsage.java

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

src/main/java/com/tutorial/part2/exercise/File.java

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

0 commit comments

Comments
 (0)