Skip to content

Commit b3c19e9

Browse files
added minor example
1 parent 3f3e469 commit b3c19e9

1 file changed

Lines changed: 8 additions & 0 deletions

File tree

liquidjava-example/src/main/java/testSuite/CorrectIfThen.java

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,14 @@ public void have1(int a) {
2525
int u = pos;
2626
}
2727

28+
public void haveAnd(int a, @Refinement("b > 5")int b) {
29+
@Refinement("pos > 0")
30+
int pos = 10;
31+
if (a > 0 && b > 0) {
32+
if (a > b) pos = a - b;
33+
}
34+
}
35+
2836
public static void main(String[] args) {
2937
@Refinement("_ < 10")
3038
int a = 5;

0 commit comments

Comments
 (0)