Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Machines

Many rows have a status that moves in one direction: an order is placed, then paid, then packed, then shipped, and may be cancelled until it ships. Written as guards, that rule is repeated in every contract that touches the status, and forgotten in one of them. A machine writes it once, as the legal moves of one field, and the language refuses every other move.

enum Status { placed, paid, packed, shipped, cancelled }
row Order { id: id, status: Status, total: money(2) }
unit Orders {
    state orders: Order[8];
    machine orders.status {
        start Status.placed;
        Status.placed -> Status.paid;
        Status.paid -> Status.packed;
        Status.packed -> Status.shipped;
        Status.placed -> Status.cancelled;
        Status.paid -> Status.cancelled;
        Status.packed -> Status.cancelled;
    }
    contract place(order: id, total: money(2)) {
        case total <= 0 => fail Empty;
        else => Placed: orders += [Order { id: order, status: Status.placed, total: total }];
    }
    contract advance(order: id, to: Status) {
        else => Moved: orders[order].status := to;
        examples {
            { orders: [Order { id: 1, status: Status.placed, total: 500 }] } (1, Status.paid)
                => Moved { orders: [Order { id: 1, status: Status.paid, total: 500 }] };
            { orders: [Order { id: 1, status: Status.packed, total: 500 }] } (1, Status.cancelled)
                => Moved { orders: [Order { id: 1, status: Status.cancelled, total: 500 }] };
            { orders: [Order { id: 1, status: Status.placed, total: 500 }] } (1, Status.shipped) => WrongStatus;
            { orders: [Order { id: 1, status: Status.paid, total: 500 }] } (1, Status.paid) => WrongStatus;
            { orders: [Order { id: 1, status: Status.shipped, total: 500 }] } (1, Status.cancelled) => WrongStatus;
        }
    }
}
scenario one_order {
    Orders.place(1, 2500) => Placed;
    Orders.advance(1, Status.shipped) => WrongStatus;
    Orders.advance(1, Status.paid) => Moved;
    Orders.advance(1, Status.paid) => WrongStatus;
    Orders.advance(1, Status.packed) => Moved;
    Orders.advance(1, Status.shipped) => Moved;
    Orders.advance(1, Status.cancelled) => WrongStatus;
}

The declaration

machine orders.status { … } names a field of a table’s rows and lists what may happen to it:

  • start Status.placed; is the only value a new row may have in that field;
  • Status.placed -> Status.paid; is one legal move, an edge, from one value to another.

Any other move is illegal. An order cannot go from placed to shipped, cannot come back from shipped, cannot be cancelled once it has shipped, because no edge says it may.

WrongStatus without a guard

advance has no guard at all. It sets the status to whatever it is asked, and the machine decides:

scenario one_order
  Orders.place(1, 2500) => Placed
  Orders.advance(1, shipped) => WrongStatus
  Orders.advance(1, paid) => Moved
  Orders.advance(1, paid) => WrongStatus
  Orders.advance(1, packed) => Moved
  Orders.advance(1, shipped) => Moved
  Orders.advance(1, cancelled) => WrongStatus
  Orders = Orders { orders: [Order { id: 1, status: shipped, total: 2500 }] }
7 step(s), all as expected

Skipping from placed to shipped answers WrongStatus. So does cancelling a shipped order at the end. WrongStatus is the fourth of the implicit outcomes from the chapter on rows: produced by the language, a failure that changes nothing, available to every contract of a unit with a machine, and nameable in examples and scenarios without a case declaring it.

That is why one contract, advance(order, to), replaces a contract per transition. Without the machine you would write pay, pack, ship and cancel, each with a guard on the current status; with it, the guards are the edges, and they are in one place. A contract that wants a different answer for an illegal move, fail NotPaidYet say, keeps its own case, tried before the delta.

Staying in place is a move

The fourth step asks to pay an order that is already paid, and the answer is WrongStatus. Assigning a field the value it already has is still a move under the machine, from paid to paid, and there is no such edge. This is deliberate: a second payment is usually a mistake worth hearing about, and a machine that wants to allow it says so with Status.paid -> Status.paid;.

Ranges

When the field is a bounded int rather than an enum, a range of values may share an edge (book/programs/machines-steps.vish):

row Ticket { id: id, step: int(1, 5) }
unit Desk {
    state tickets: Ticket[8];
    machine tickets.step { start 1; 1 -> 2; 2 -> 3; 3 -> 4; 1..3 -> 5; }
    contract open(ticket: id, step: int(1, 5)) {
        else => Opened: tickets += [Ticket { id: ticket, step: step }];
        examples {
            {} (1, 1) => Opened { tickets: [Ticket { id: 1, step: 1 }] };
            {} (1, 3) => WrongStatus;
        }
    }
    contract advance(ticket: id, to: int(1, 5)) {
        else => Moved: tickets[ticket].step := to;
        examples {
            { tickets: [Ticket { id: 1, step: 2 }] } (1, 5) => Moved { tickets: [Ticket { id: 1, step: 5 }] };
            { tickets: [Ticket { id: 1, step: 4 }] } (1, 5) => WrongStatus;
        }
    }
}

1..3 -> 5 is three edges at once: from any step from one to three, a ticket may jump to five. From step four it may not, which the last example states. The examples of open show start at work: a new ticket at step one is fine, and a new ticket at step three is WrongStatus. With an enum status, as in the orders, each edge is written on its own line.

The sampler assumes nothing the machine excludes

The verifier draws states at random, and it draws the status of each row like any other field: any value of its type. It does not ask whether the machine could have reached that row. So a contract may not rely on the machine to rule a state out. Here is a unit that does (book/failures/machines-assume.vish):

enum Status { placed, paid, shipped }
row Order { id: id, status: Status, total: money(2), paid: money(2) }
unit Orders {
    state orders: Order[8];
    machine orders.status { start Status.placed; Status.placed -> Status.paid; Status.paid -> Status.shipped; }
    contract place(order: id, total: money(2)) => Placed: orders += [Order { id: order, status: Status.placed, total: total, paid: 0 }];
    contract pay(order: id) => Paid: orders[order].status := Status.paid, orders[order].paid := orders[order].total;
    contract ship(order: id) {
        else => Shipped: orders[order].status := Status.shipped;
        ensures orders[order].paid == orders[order].total;
        examples {
            { orders: [Order { id: 1, status: Status.paid, total: 500, paid: 500 }] } (1)
                => Shipped { orders: [Order { id: 1, status: Status.shipped, total: 500, paid: 500 }] };
        }
    }
}

pay moves an order to paid and records the payment in the same call, so every paid order the scenarios could produce has paid == total, and ship says so in an ensures, a check on the state after the call. The verifier disagrees:

verify FAILED: 1 failure(s):
[1] sampled check failed: Orders.ship: Orders.ship: ensures of case 1 violated: state Orders { orders: [Order { id: 0, status: placed, total: -59, paid: 13 }, Order { id: 3, status: shipped, total: 25, paid: 20 }, Order { id: 4, status: shipped, total: 62, paid: 51 }, Order { id: 5, status: placed, total: -39, paid: 29 }, Order { id: 6, status: paid, total: 4, paid: 36 }] } args (3,) out Shipped
  (state Orders { orders: [Order { id: 0, status: placed, total: -59, paid: 13 }, Order { id: 3, status: paid, total: 25, paid: 20 }, Order { id: 4, status: shipped, total: 62, paid: 51 }, Order { id: 5, status: placed, total: -39, paid: 29 }, Order { id: 6, status: paid, total: 4, paid: 36 }] } args (3,))

It drew order 3 in status paid with 20 paid of a total of 25, a row no sequence of calls produces, and shipped it. The machine allowed the move from paid to shipped; nothing said a paid order has been paid in full. The rule lived in the author’s head and in the pairing of two deltas in pay, and the verifier cannot see either.

The fix is to state it as a rule about every state: add invariant all(o in orders: o.status == Status.placed || o.paid == o.total); to the unit. Now the verifier draws only states that keep the invariant, checks that pay and ship keep it too, and the program verifies.

verify: 5 examples, 7 scenario steps and 4000 sampled checks passed

Try

Add the edge Status.paid -> Status.paid; to the orders machine. The program checks, and the run stops at the fourth step: it expected WrongStatus for the second payment and got Moved. vishy verify also fails the example that says paying a paid order is WrongStatus. The machine is the rule, and the examples and the scenario are how you know it is the rule you meant.