liquidjava/liquidjava-example/src/main/java/testingInProgress/OrderSimple.java at e3d8bc1b5163321c227e757cf576b5bf88802c42 · liquid-java/liquidjava · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
package testingInProgress;

import liquidjava.specification.RefinementPredicate;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"empty", "addingItems", "checkout", "closed"})
@RefinementPredicate("int countItems(OrderSimple o)")
public class OrderSimple {

    @StateRefinement(to = "(countItems(this) == 0) && empty(this)")
    public OrderSimple() {}

    @StateRefinement(
            from = "(empty(this) || addingItems(this))",
            to = "((countItems(this) == (countItems(old(this)) + 1)) && addingItems(this))")
    //	@Refinement("_ == this")
    public OrderSimple addItem(String itemName, int price) {
        return this;
    }

    @StateRefinement(from = "((addingItems(this)) && (countItems(this) > 20))")
    public boolean hasGift() {
        return true;
    }

    //	@StateRefinement(from="addingItems(this)", to = "checkout(this)")
    //	public Order pay(int cardNumber) {
    //		return this;
    //	}

    //	@StateRefinement(from="checkout(this) && priceNow(this) > 20", to = "checkout(this)")
    //	public Order addGift() {
    //		return this;
    //	}
    //
    //	@StateRefinement(from="checkout(this)", to = "closed(this)")
    //	public Order sendToAddress(String a) {
    //		return this;
    //	}

}