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