Examples

A scenario says what a sequence of calls does from the first state. An example says what one call does from a state you choose. Examples live inside the contract they test, and they are the contract’s acceptance tests: the person who writes the header writes them, and the body is not done until every one of them passes.

row Book { id: id, title: string(32), copies: int(0, 9) }
unit Library {
    state books: Book[8];
    state loans: int = 0;
    contract shelve(book: id, title: string(32), copies: int(1, 9)) {
        else => Shelved: books += [Book { id: book, title: title, copies: copies }];
        examples {
            {} (1, "Dune", 2) => Shelved { books: [Book { id: 1, title: "Dune", copies: 2 }] };
        }
    }
    contract lend(book: id) -> int {
        case books[book].copies == 0 => fail NoCopy;
        else => Lent(books[book].copies - 1): books[book].copies -= 1, loans += 1;
        examples {
            { books: [Book { id: 1, title: "Dune", copies: 2 }] } (1) => Lent(1) { books: [Book { id: 1, title: "Dune", copies: 1 }], loans: 1 };
            { books: [Book { id: 1, title: "Dune", copies: 1 }], loans: 4 } (1) => Lent(0) { books: [Book { id: 1, title: "Dune", copies: 0 }], loans: 5 };
            { books: [Book { id: 1, title: "Dune", copies: 0 }] } (1) => NoCopy;
        }
    }
    contract on_loan() -> int {
        else => OnLoan(loans);
        examples {
            { loans: 3 } () => OnLoan(3);
        }
    }
}
scenario one_copy {
    Library.shelve(1, "Dune", 1) => Shelved;
    Library.lend(1) => Lent(0);
    Library.lend(1) => NoCopy;
    Library.on_loan() => OnLoan(1);
}

The shape of an example

An example is one line: a state before the call, the arguments, the outcome that must come back, and, for a success, what the state must be after.

{ books: [Book { id: 1, title: "Dune", copies: 2 }] } (1) => Lent(1) { books: [...], loans: 1 };

Read it left to right: from a library holding two copies of one book, lend(1) must answer Lent carrying 1, the copies left, and afterwards the book has one copy and one loan is counted. Each example starts fresh from its own before-state; examples do not run in sequence and do not see each other.

The state literal

The braces before the arguments are a state literal: it names fields of the unit and gives them values. A field it does not name has its initial value. So { loans: 3 } is a library with no books and three loans, and {} is the unit as it starts. You write only the part of the state the example is about, and the rest is the empty library every reader already knows.

A field that is a table is given whole: books: [Book { … }] is the entire table, one row.

The after-state says what changed

The braces after the outcome are the after-state, and they are read differently: a field the after-state does not name is unchanged by the call. The second lend example starts with four loans and ends with five, and it must say so, loans: 5; if the call had not touched loans, the example would leave it out.

This is the second of the language’s two removals seen from the test side. A contract changes nothing its deltas do not name, and an example says nothing about what did not change. So an example with no after-state at all, like on_loan’s, is a claim that the call changed nothing. The verifier holds you to that claim.

A carried value

Lent(1) and OnLoan(3) give the carried value the call must produce. The value is compared exactly, so an example pins the formula down at one point: Lent(books[book].copies - 1) from two copies must be 1, computed on the state before the call.

A failure

{ books: [Book { id: 1, title: "Dune", copies: 0 }] } (1) => NoCopy; is a failure example. It has no after-state, because a failure changes nothing and so there is nothing to say about the state afterwards.

What the tools do with them

vishy verify runs every example before it samples anything:

verify: 5 examples, 4 scenario steps and 6000 sampled checks passed

Five examples: one for shelve, three for lend, one for on_loan. The scenario then runs from the empty library:

scenario one_copy
  Library.shelve(1, "Dune", 1) => Shelved
  Library.lend(1) => Lent(0)
  Library.lend(1) => NoCopy
  Library.on_loan() => OnLoan(1)
  Library = Library { books: [Book { id: 1, title: "Dune", copies: 0 }], loans: 1 }
4 step(s), all as expected

The checker reads the examples too, before anything runs. An example that names an outcome the contract does not have is refused, so a misspelled outcome is found at the line that misspells it (book/refusals/examples-outcome.vish):

book/refusals/examples-outcome.vish:9:74: error: `NoCopies` is not an outcome of `lend`
              { books: [Book { id: 1, title: "Dune", copies: 0 }] } (1) => NoCopies;
                                                                           ^^^^^^^^

An example that says too little

Here is a contract that returns a book, with an example that forgets to say what changed (book/failures/examples-silent.vish):

row Book { id: id, title: string(32), copies: int(0, 9) }
unit Library {
    state books: Book[8];
    state loans: int = 0;
    contract give_back(book: id) {
        else => Returned: books[book].copies += 1, loans -= 1;
        examples {
            { books: [Book { id: 1, title: "Dune", copies: 0 }], loans: 1 } (1) => Returned;
        }
    }
}

The checker accepts it. The verifier does not:

verify FAILED: 1 failure(s):
[1] Library.give_back example 1: the example gives no after-state, which means unchanged, but the state changed: before Library { books: [Book { id: 1, title: "Dune", copies: 0 }], loans: 1 } after Library { books: [Book { id: 1, title: "Dune", copies: 1 }], loans: 0 } (write the after-state, or `unchanged`)

The example has no after-state, so it claims that returning a book changes nothing. The call added a copy and took a loan away, and the verifier prints both states so you can see which. The fix is to write what changed: => Returned { books: [Book { id: 1, title: "Dune", copies: 1 }], loans: 0 };. A success example whose contract changed the state without the example saying so always fails this way, which is what keeps examples honest as documentation: a reader of an example sees every field the call touches.

Examples and the rest of the verifier

An example is one point. The sampled checks of the earlier chapters are thousands of points nobody wrote. The two do different work. The sampled checks look for a state that breaks a rule, and this program has no rule about what Lent carries, so they have nothing to hold that number to. The examples do: they fix the answer at the states you chose, and the verifier compares it exactly.

Try

Change the first lend example’s after-state from loans: 1 to loans: 2. The program still checks; vishy verify fails on that example and prints the state it expected next to the state it got, with loans: 1 in the second. Then delete , loans: 1 from the same after-state entirely: the example now claims the call left loans at its value before the call, zero, and the verifier reports the same kind of failure, expecting loans: 0 and getting loans: 1.