Order
This example shows a more expressive protocol that combines typestates, ghost variables, and value-dependent conditions.
import liquidjava.specification.*;
@StateSet({"ordering", "checkout", "finished"})
@Ghost("int total")
public class Order {
@StateRefinement(to="ordering() && total() == 0")
public Order() {}
@Refinement("_ == this")
@StateRefinement(from="ordering()", to="ordering() && total() == total(old(this)) + price")
public Order addItem(String name, @Refinement("_ > 0") int price) { return this; }
@Refinement("_ == this")
@StateRefinement(from="ordering() && total() > 0", to="checkout() && total() == total(old(this))")
public Order checkout() { return this; }
@Refinement("_ == this")
@StateRefinement(from="checkout() && amount == total()", to="finished()")
public Order pay(@Refinement("_ > 0") int amount) { return this; }
}
Order order = new Order();
order.addItem("shirt", 60)
.addItem("shoes", 80)
.checkout()
.pay(140);
Order order = new Order();
order.addItem("shirt", 60)
.addItem("shoes", 80)
.checkout()
.pay(120); // State Refinement Error
This example enforces the intended protocol:
- Items can only be added in the
ordering state, and the total is updated accordingly
- The
checkout method can only be called after at least one item has been added, and the total must remain the same
- The
pay method can only be called after checkout, and the amount must match the order total