Skip to content

Commit 617ca53

Browse files
CatarinaGamboaCatarinaGamboa
committed
changes
1 parent 9fcd169 commit 617ca53

File tree

12 files changed

+42
-71
lines changed

12 files changed

+42
-71
lines changed

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ You can find out more about LiquidJava in the following resources:
3434

3535
## Run verification
3636
#### In a specific project
37-
Run the file `liquidjava-verifier\api\CommandLineLaucher` with the path to the target project for verification.
37+
Run the file `liquidjava-verifier\api\CommandLineLauncher` with the path to the target project for verification.
3838
If there are no arguments given, the application verifies the project on the path `liquidjava-example\src\main\java`.
3939

4040

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

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

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

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,24 @@
44

55
class SimpleTest {
66

7-
@Refinement("return > 0")
7+
@Refinement("return < 0")
88
public int test() {
99
return 10;
1010
}
1111
}
1212

13+
14+
15+
16+
17+
18+
19+
20+
21+
22+
23+
24+
1325
// @RefinementAlias("Percentage(int x) { 0 <= x && x <= 100 }")
1426
// @Refinement("Percentage(_)")
1527
// public static int addBonus(

‎liquidjava-example/src/main/java/testingInProgress/Account.java‎

Lines changed: 20 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,26 @@
11
package testingInProgress;
22

3-
import liquidjava.specification.Ghost;
4-
import liquidjava.specification.Refinement;
5-
import liquidjava.specification.StateRefinement;
3+
// import liquidjava.specification.Ghost;
4+
// import liquidjava.specification.StateRefinement;
5+
// import liquidjava.specification.StateSet;
66

7-
@Ghost("int sum")
7+
// @Ghost("int amount")
8+
// @StateSet({"positive", "negative"})
89
public class Account {
9-
10-
@Refinement("balance >= 0")
11-
private int balance;
12-
13-
public Account() {
14-
balance = 0;
15-
}
16-
17-
@StateRefinement(to = "sum(this) == v")
18-
public Account(@Refinement("v >= 0") int v) {
19-
balance = v;
20-
}
21-
22-
@StateRefinement(
23-
to = "(sum(old(this)) > v)? (sum(this) == (sum(old(this)) - v)) : (sum(this) == 0)")
24-
public void withdraw(int v) {
25-
if (v > balance) balance = 0;
26-
else balance = balance - v;
27-
}
28-
29-
@StateRefinement(to = "sum(this) == (sum(old(this)) + v)")
30-
public void deposit(int v) {
31-
balance += v;
32-
}
33-
34-
// @StateRefinement(from="(amount <= sum(this)) && (sum(this) == sum(old(this)))", to="...")
35-
// @Refinement("sum(_) == (sum(old(_)) + amount)")
36-
// public Account transferTo(Account other, @Refinement("_ < sum(this)")int amount) {
37-
// this.withdraw(amount);
38-
// other.deposit(amount);
39-
// return other;
40-
// }
10+
// int qnt;
11+
//
12+
// @StateRefinement(from="positive(this)",
13+
// to="(amount(this) == amount(old(this)) - x) && " +
14+
// "(amount(this) < 0? negative(this):positive(this))")
15+
//// @StateRefinement(to="(amount(this) == amount(old(this)) - x)")
16+
// public int withdraw(int x) {
17+
// qnt -= x;
18+
// return qnt;
19+
// }
20+
//
21+
// @StateRefinement(to="amount(this) == amount(old(this)) + x")
22+
// public void add(int x) {
23+
// qnt += x;
24+
// }
4125

4226
}

liquidjava-example/src/main/java/test/currentlyTesting/AccountClient.java renamed to liquidjava-example/src/main/java/testingInProgress/AccountClient.java

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

33
// @StateSet({"active", "inactive"})
44
public class AccountClient {

liquidjava-example/src/main/java/test/currentlyTesting/CommitAndRedirectSimulation.java renamed to liquidjava-example/src/main/java/testingInProgress/CommitAndRedirectSimulation.java

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

33
import java.io.PrintWriter;
44

liquidjava-example/src/main/java/test/currentlyTesting/IteratorRefinements.java renamed to liquidjava-example/src/main/java/testingInProgress/IteratorRefinements.java

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

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

liquidjava-example/src/main/java/test/currentlyTesting/LinkedListRefinements.java renamed to liquidjava-example/src/main/java/testingInProgress/LinkedListRefinements.java

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

33
import java.util.Iterator;
44

liquidjava-example/src/main/java/test/currentlyTesting/TestIterator.java renamed to liquidjava-example/src/main/java/testingInProgress/TestIterator.java

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

33
import java.io.File;
44
import java.io.FileInputStream;

liquidjava-example/src/main/java/test/currentlyTesting/testFile.txt renamed to liquidjava-example/src/main/java/testingInProgress/testFile.txt

File renamed without changes.

0 commit comments

Comments
 (0)