Process anti-patterns

Mistakes in how a team or a writer stage uses the tools: a verdict sent to the wrong owner, a change made in one place, a pattern left for every writer to rediscover, a pass read as more than it says. Four items, each with a program the guide’s check runs.

Repairing the writer when the verdict names a missing outcome

Problem

A verdict names a contract, so it goes back to the contract’s writer. But some verdicts that name a contract are the interface’s fault: a rule the invariant states has no outcome in the contract’s signature, so no body can keep the rule and be accepted. The writer adds the guard the rule needs and is refused for producing an outcome the interface did not declare; leaves it out and is failed by the invariant. In the experiments that shaped the language, three signatures lacked such an outcome, and every writer invented a name for it until the outcome gate refused them. Sending the verdict to the writer again is a repair round that cannot succeed; the fix is one line in the interface, and it is the interface owner’s.

Example

unit Account {
    state balance: money(2) = 0;
    invariant balance >= 0;
    contract withdraw(amount: money(2)) {
        // Withdrawn: the balance goes down by amount.
        outcomes Withdrawn, fail BadAmount;
        examples { { balance: 500 } (200) => Withdrawn { balance: 300 }; { balance: 500 } (0) => BadAmount; }
    }
}
flow withdraw(amount: money(2)) atomic { Account.withdraw(amount); }
unit Account {
    contract withdraw(amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        else => Withdrawn: balance -= amount;
    }
}

The interface (the first block) promises a balance that never goes negative and declares no failure for an amount the balance cannot cover. The part (the second block) is the honest body; the verifier fails it:

verify FAILED: 2 failure(s):
[1] sampled check failed: Account.withdraw: Account.withdraw: invariant violated after case 2: state Account { balance: -13 } args (26,)
  (state Account { balance: 13 } args (26,))
[2] flow withdraw: Account.withdraw: invariant violated after case 2: state Account { balance: -51 } args (51,)
  (world World { account: Account { balance: 0 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (51,))

The writer who reads that verdict and adds the guard is refused (the program is book/refusals/anti-repair-guess.vish):

book/refusals/anti-repair-guess.vish:14:39: error: `Account.withdraw` produces `Insufficient`, which the interface does not declare (declared: Withdrawn, BadAmount; implicit: Unknown, Exists, Full, WrongStatus)
          case amount > balance => fail Insufficient;
                                        ^^^^^^^^^^^^

Both verdicts name Account.withdraw. Neither is the writer’s to fix.

Refactoring

unit Account {
    state balance: money(2) = 0;
    invariant balance >= 0;
    contract withdraw(amount: money(2)) {
        // Withdrawn: the balance goes down by amount; Insufficient when amount exceeds it.
        outcomes Withdrawn, fail BadAmount, fail Insufficient;
        examples { { balance: 500 } (200) => Withdrawn { balance: 300 }; { balance: 500 } (0) => BadAmount; { balance: 100 } (200) => Insufficient; }
    }
}
flow withdraw(amount: money(2)) atomic { Account.withdraw(amount); }
unit Account {
    contract withdraw(amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        case amount > balance => fail Insufficient;
        else => Withdrawn: balance -= amount;
    }
}

verify: 3 examples, 0 scenario steps and 2000 sampled checks passed

The interface declares Insufficient with the example that produces it, and the same part passes. The rule for routing a verdict: an invariant broken by a contract that has no outcome for the rule goes to the interface owner first; a failed example or a refused outcome on a contract that does declare the outcome goes to the writer.

Additional remarks

A verdict that names a contract whose interface already declares the right outcome, with its example, is the writer’s, and the writer stage’s repair rounds handle it. The item is about the verdicts that look like the writer’s and are not.

A changed flow without its flows and scenarios restated

Problem

A requirement arrives in installments, or an interface is edited after scenarios were written. A flow gains a parameter or changes its order of calls; the scenarios and the other flows that call it are kept as they were. The checker refuses the kept scenario, which is the cheap case; the expensive case is a kept scenario that still types and now states behaviour the changed flow no longer has, or a kept flow that no longer keeps a rule the change added. In the experiments that shaped the language, twenty-five of thirty-one assembly failures in one run were one account’s new rule that no kept flow exercised. A change to a flow restates, in the same place, every flow and scenario that exercises it.

Example

row Booking { id: id, room: id, day: int(1, 366), slot: int(1, 8) }
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, day: int(1, 366), slot: int(1, 8)) {
        else => Booked: bookings += [Booking { id: booking, room, day, slot }];
    }
}
flow book(booking: id, room: id, day: int(1, 366), slot: int(1, 8)) atomic { Bookings.book(booking, room, day, slot); }
scenario kept_from_before { book(1, 1, 10) => Booked; }

book/refusals/anti-stale-scenario.vish:9:29: error: scenario `kept_from_before` step 1: `book` takes 4 argument(s), got 3
  scenario kept_from_before { book(1, 1, 10) => Booked; }
                              ^^^^^^^^^^^^^^^^^^^^^^^^^

Refactoring

row Booking { id: id, room: id, day: int(1, 366), slot: int(1, 8) }
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, day: int(1, 366), slot: int(1, 8)) {
        else => Booked: bookings += [Booking { id: booking, room, day, slot }];
    }
}
flow book(booking: id, room: id, day: int(1, 366), slot: int(1, 8)) atomic { Bookings.book(booking, room, day, slot); }
scenario restated { book(1, 1, 10, 2) => Booked; }

verify: 0 examples, 1 scenario steps and 2000 sampled checks passed

The scenario is restated with the slot the flow now takes. When the change is to a rule rather than a signature, nothing refuses the stale scenario, and restating it is the only check: read every scenario that calls the flow, and every flow that commands a unit the rule couples, and say again what each does under the new rule.

Additional remarks

A scenario that the change does not reach (it calls other flows, on other units) is kept as it is. The item is about the ones that exercise what changed.

Idioms left unnamed for writers

Problem

A rule in an interface needs a pattern to write: a quota spread over rows in order, a selection by rank with ties broken, a removal by a computed list. A writer who is not told the pattern’s name and shape invents one, and the verifier refuses the inventions one by one. The quota-over-rows pattern cost twelve writer rounds before the writer reference stated it; the next writer passed in one. The interface owner names the idiom in the rule’s comment, and the pattern is in the reference the writers receive.

Example

row Batch { id: id, sku: id, qty: int(0, 99) }
unit Stock {
    state batches: Batch[8];
    fixture Three = { batches: [Batch { id: 1, sku: 7, qty: 5 }, Batch { id: 2, sku: 7, qty: 3 }, Batch { id: 3, sku: 8, qty: 4 }] };
    invariant all(b in batches: b.qty >= 0);
    contract take(sku: id, qty: int(1, 99)) {
        // Short when the sku's batches hold fewer than qty in total; else qty is taken from the batches, the oldest first, each giving what it has until qty is met.
        outcomes Taken, fail Short;
        examples {
            Three (7, 6) => Taken { batches: [Batch { id: 1, sku: 7, qty: 0 }, Batch { id: 2, sku: 7, qty: 2 }, Batch { id: 3, sku: 8, qty: 4 }] };
            Three (7, 9) => Short;
        }
    }
}
flow take_stock(sku: id, qty: int(1, 99)) atomic { Stock.take(sku, qty); }

ok: 1 row(s), 0 event(s), 0 fn(s), 1 unit(s), 1 contract(s), 1 flow(s)

Nothing catches it; the interface is complete and its examples pin the answer. The sentence “the oldest first, each giving what it has until qty is met” is a specification of a delta that the language writes in one particular way, and the writer has to find that way.

Refactoring

row Batch { id: id, sku: id, qty: int(0, 99) }
unit Stock {
    state batches: Batch[8];
    fixture Three = { batches: [Batch { id: 1, sku: 7, qty: 5 }, Batch { id: 2, sku: 7, qty: 3 }, Batch { id: 3, sku: 8, qty: 4 }] };
    invariant all(b in batches: b.qty >= 0);
    contract take(sku: id, qty: int(1, 99)) {
        // Short when the sku's batches hold fewer than qty in total; else the quota-over-rows pattern, oldest first
        // (writer reference): each batch gives up what is left of qty after the batches before it.
        case sum(where(b in batches: b.sku == sku).qty) < qty => fail Short;
        else => Taken: batches := for b where b.sku == sku => with(b, qty, b.qty - clamp(qty - sum(where(c in batches: c.sku == sku && as_int(c.id) < as_int(b.id)).qty), 0, b.qty));
        examples {
            Three (7, 6) => Taken { batches: [Batch { id: 1, sku: 7, qty: 0 }, Batch { id: 2, sku: 7, qty: 2 }, Batch { id: 3, sku: 8, qty: 4 }] };
            Three (7, 9) => Short;
            Three (8, 4) => Taken { batches: [Batch { id: 1, sku: 7, qty: 5 }, Batch { id: 2, sku: 7, qty: 3 }, Batch { id: 3, sku: 8, qty: 0 }] };
        }
    }
}
flow take_stock(sku: id, qty: int(1, 99)) atomic { Stock.take(sku, qty); }

verify: 3 examples, 0 scenario steps and 2000 sampled checks passed

The comment names the pattern and where it is written down, and the body is the pattern as the reference states it: each row gives up what is left of the quota after the rows before it, so one set-valued delta does the whole thing. The third example, on the other sku, is the one a writer most often gets wrong (the untouched batches must stay untouched).

Additional remarks

The item is for the interface owner and for whoever keeps the writer reference: a pattern that took a writer more than one round is a paragraph the reference is missing. A pattern the reference already names is the writer’s to look up.

A pass on the exampled states read as a pass on all states

Problem

verify ends with one line: so many examples, so many scenario steps, so many sampled checks passed. It is read as “the program is correct”. It says three narrower things: the examples agree with the bodies; the scenarios ran as stated; in the sampled states, no rule the program states was broken. A carried value with no property, a rule left in prose, a fact hidden in an effect, all pass, because there was nothing for the sample to break. The cost is confidence in the wrong place: the program is trusted for what nobody asked it to keep.

Example

row Room { id: id, closed: bool }
unit Rooms {
    state rooms: Room[8];
    fixture Two = { rooms: [Room { id: 1, closed: false }, Room { id: 2, closed: false }] };
    contract close(room: id) {
        else => Closed: rooms[room].closed := true;
        examples { Two (1) => Closed { rooms: [Room { id: 1, closed: true }, Room { id: 2, closed: false }] }; }
    }
    contract open_count() -> int {
        else => Count(len(rooms));
        examples { {} () => Count(0); Two () => Count(2); }
    }
}

verify: 3 examples, 0 scenario steps and 2000 sampled checks passed

open_count counts closed rooms as open. Three examples and two thousand sampled checks passed. The sampled checks held the unit to its invariant, and it has none; the examples were on states with no closed room. The line is true and the program is wrong.

Refactoring

row Room { id: id, closed: bool }
unit Rooms {
    state rooms: Room[8];
    fixture Two = { rooms: [Room { id: 1, closed: false }, Room { id: 2, closed: false }] };
    contract close(room: id) {
        else => Closed: rooms[room].closed := true;
        examples { Two (1) => Closed { rooms: [Room { id: 1, closed: true }, Room { id: 2, closed: false }] }; }
    }
    contract open_count() -> int {
        ensures result == count(r in rooms: !r.closed);
        else => Count(count(r in rooms: !r.closed));
        examples { {} () => Count(0); Two () => Count(2); }
    }
}

verify: 3 examples, 0 scenario steps and 2000 sampled checks passed

The same line, one more example, and now it means something: the property on open_count is a rule the sample could have broken and did not. The Contract page showed the wrong body failing under that property on a state with four closed rooms. What the pass covers is decided by what the program states, not by the number at the end of the line.

Additional remarks

Read the line as a report of what was tried. Then read the program for what it does not state: a carried value without a property, a rule in a comment, an effect with a rule inside, a table bound smaller than the state the bug needs. The chapter “What the verifier cannot see” lists the four holes, two of which now have a check; the other two are the reader’s. Before serving, run the verifier on three seeds and at three thousand iterations, as the handbook says: a program has passed at one thousand and failed at three.