Skip to content

order.md

Latest commit

 

History

History
52 lines (42 loc) · 1.53 KB

order.md

File metadata and controls

52 lines (42 loc) · 1.53 KB
title Order
parent Examples
nav_order 5
permalink /examples/order/
description A typestate protocol for a simple order processing system.

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() {}

    @StateRefinement(from="ordering()", to="ordering() && total() == total(old(this)) + price")
    public Order addItem(String name, @Refinement("_ > 0") int price) {}

    @StateRefinement(from="ordering() && total() > 0", to="checkout() && total() == total(old(this))")
    public Order checkout() {}

    @StateRefinement(from="checkout() && amount == total()", to="finished()")
    public Order pay(@Refinement("_ > 0") int amount) {}
}
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