Order

Shopping-order protocol with typestate + price ghost (LiquidJava ``Order``). States (boolean measures): empty → adding (via add_item) → checkout (via pay) → closed (via ship) ``total_price`` tracks the sum of item prices. ``add_gift`` is only legal in checkout when ``total_price > 20``. The order handle is linear.
Table of Contents

Types

Order

(type) linear
linear type Order

Functions

new_order

Fresh empty order with price 0.
def new_order (_ : Unit) : {o : Order | empty o = true && adding o = false && checkout o = false && closed o = false && total_price o = 0}

add_item

Add a positively priced item (empty or adding → adding).
def add_item (name : String | name ≠ "") (price : Int | price > 0) (1 o : Order | empty o = true || adding o = true) : { out : Order | empty out = false && adding out = true && checkout out = false && closed out = false && total_price out = total_price o + price }

pay

Pay and enter checkout (adding → checkout); price unchanged.
def pay (card : Int | card > 0) (1 o : Order | adding o = true) : { out : Order | empty out = false && adding out = false && checkout out = true && closed out = false && total_price out = total_price o }

add_gift

Optional gift in checkout when the cart totals more than 20.
def add_gift (1 o : Order | checkout o = true && total_price o > 20) : {out : Order | checkout out = true && closed out = false && total_price out = total_price o}

ship

Ship to an address (checkout → closed).
def ship (address : String | address ≠ "") (1 o : Order | checkout o = true) : {out : Order | checkout out = false && closed out = true && total_price out = total_price o}

finalize

Consume a closed order; returns the final total.
def finalize (1 o : Order | closed o = true) : {n : Int | n = total_price o && n ≥ 0}

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

empty

uninterpreted
def empty : (o : Order) → Bool

adding

uninterpreted
def adding : (o : Order) → Bool

checkout

uninterpreted
def checkout : (o : Order) → Bool

closed

uninterpreted
def closed : (o : Order) → Bool

total_price

uninterpreted
def total_price : (o : Order) → Int