Scenarios
The verifier samples states nobody wrote down, and that finds the call that breaks a rule. It cannot know what the program is for. A scenario says that: a short story of calls from the initial world, each with the outcome it must produce. It is the program’s behavioural specification, what the product does in the order a person would do it, and every vishy verify runs it.
row Book { id: id, lent: bool }
row Loan { id: id, book: id, reader: id, due: instant }
unit Shelf {
state books: Book[4];
contract add(book: id) => Added: books += [Book { id: book, lent: false }];
contract lend(book: id) {
case !(book in books) => fail NoSuchBook;
case books[book].lent => fail OnLoan;
else => Lent: books[book].lent := true;
}
contract take_back(book: id) => Returned: books[book].lent := false;
}
unit Loans {
state loans: Loan[4];
contract open(loan: id, book: id, reader: id, due: instant) -> id => Opened(loan): loans += [Loan { id: loan, book, reader, due }];
contract close(loan: id, reader: id) -> id {
case !(loan in loans) => fail NoSuchLoan;
case loans[loan].reader != reader => fail NotYours;
else => Closed(loans[loan].book): remove loans[loan];
}
}
flow borrow(book: id) uses clock, ids, caller atomic {
let loan = fresh();
Shelf.lend(book);
Loans.open(loan, book, caller, now + days(14));
}
flow give_back(loan: id) uses caller atomic {
let book = Loans.close(loan, caller);
Shelf.take_back(book);
}
scenario a_fortnight {
Shelf.add(1) => Added;
at 1000 as 7 borrow(1) => Opened(loan);
as 8 borrow(1) => OnLoan;
as 8 give_back(loan) => NotYours;
as 7 give_back(loan) => Returned;
at 2000 as 8 borrow(1) => Opened(_);
as 8 borrow(2) => NoSuchBook;
}
Steps
Each step is a call and the outcome it must produce: as 8 borrow(1) => OnLoan;. The steps run in order, starting from the initial world, each on the world the previous one left.
A step calls a flow by name, or a contract directly. Shelf.add(1) has no flow written around it; the scenario runs it as a flow of one call, atomic like any other. The checker counts it among the flows: the program declares two, and the answer says three.
ok: 2 row(s), 0 event(s), 0 fn(s), 2 unit(s), 5 contract(s), 3 flow(s)
The clock and the caller
A flow that says uses clock reads the time as now, and one that says uses caller reads who called as caller. In a scenario both are written in the step: at 1000 sets the clock and as 7 sets the caller, so the story runs the same way every time. Reader 7 borrows at 1000, reader 8 is refused the same book, and each give_back is judged by who asks.
Carried values: a value, any value, a name
When an outcome carries a value, a step can state it exactly, Opened(10); accept any value with _, Opened(_); or bind it to a name, Opened(loan), which later steps pass as an argument.
Binding is how a scenario follows an id it cannot know. borrow draws the loan’s id with fresh(), an id no table holds, and a scenario has no way to predict which one that will be. Step 2 binds it as loan; steps 4 and 5 give it back, once as the wrong reader and once as the right one.
What run prints
vishy run executes every scenario and prints the trace:
scenario a_fortnight
Shelf.add(1) => Added
borrow(1) => Opened(10)
borrow(1) => OnLoan
give_back(10) => NotYours
give_back(10) => Returned
borrow(1) => Opened(0)
borrow(2) => NoSuchBook
Shelf = Shelf { books: [Book { id: 1, lent: true }] }
Loans = Loans { loans: [Loan { id: 0, book: 1, reader: 8, due: 1209602000 }] }
7 step(s), all as expected
Each step is printed with the outcome it produced, and a bound name is shown by its value: the loan was 10, so give_back(loan) appears as give_back(10). After the steps comes every unit’s state as the story left it. Read it as the story’s record: the book is lent again, and the one open loan is reader 8’s, due fourteen days after 2000, in milliseconds. The verifier counts the same seven steps:
verify: 0 examples, 7 scenario steps and 8000 sampled checks passed
The first wrong step
Write the scenario the way a programmer used to auto-increment keys would, expecting the first loan to be number 1 (the program is book/failures/scenarios-first-id.vish):
scenario a_fortnight {
Shelf.add(1) => Added;
at 1000 as 7 borrow(1) => Opened(1);
as 8 borrow(1) => OnLoan;
as 8 give_back(1) => NotYours;
as 7 give_back(1) => Returned;
at 2000 as 8 borrow(1) => Opened(_);
as 8 borrow(2) => NoSuchBook;
}
verify FAILED: 1 failure(s):
[1] scenario a_fortnight step 2 (borrow): expected Opened(1), got Opened(10) from Loans.open
world World { shelf: Shelf { books: [Book { id: 1, lent: true }] }, loans: Loans { loans: [Loan { id: 10, book: 1, reader: 7, due: 1209601000 }] }, __now: 1000, __ids: 0, __seed: 1442695040888963407, __caller: 7 }
The verdict names the scenario, the step, the flow, what the step expected and what came instead, and the contract call it came from: Loans.open, the flow’s last call, whose outcome is the flow’s. Then it prints the world as it stood right after that step, with the loan under its real id, 10.
The scenario stops at the first wrong step. Steps 4 and 5 give back a loan numbered 1, which does not exist, and would be wrong too, yet the verdict has one failure: steps 3 to 7 did not run. Each would be judged on a world the story did not expect, and its answer would only repeat the first mistake in other words. One wrong step, one failure, and it is the one to read.
The fix is the name. Opened(loan) binds whatever id was drawn, and the steps that follow use it.
What a scenario is for
A rule about every state belongs in an invariant or a failure case, where the verifier checks it from states nobody wrote. A scenario holds what rules cannot say: the order of a day’s events and the outcome a person sees at each one. So scenarios are few, one per behaviour the product promises, and each is short.
Try
In scenarios-library.vish, change step 2’s Opened(loan) to Opened(_). The checker refuses the program at step 4: arguments must be literals or names bound by an earlier step. Nothing bound loan any more.