Interfaces and parts

Until now one writer wrote the whole program. This part of the book is about many writers on one program at once, people or models, and it rests on the first of the language’s two removals: a unit cannot be read from outside. The appendix Building with a team tells the story on the room-booking program, with the roles, the sequence and what to do when a step fails. This chapter is the mechanism, on a smaller program: a tool library with a shelf of tools and a box of members’ cards.

Two kinds of owner

A program written by many hands has one interface owner and any number of unit owners. The interface owner writes the interface: the one shared file, holding everything the units have in common and every promise each unit makes. A unit owner writes a part: the contract bodies of one unit, and nothing else.

The interface

row Tool { id: id, kind: string(32), copies: int(1, 9), lent: int(0, 9) }
row Card { id: id, holding: int(0, 3) }

unit Shelf {
    state tools: Tool[16];
    // rule 1: a tool never has more copies lent than the shelf owns.
    invariant all(t in tools: t.lent <= t.copies);
    fixture Drill = { tools: [Tool { id: 1, kind: "drill", copies: 2, lent: 1 }] };
    contract add(tool: id, kind: string(32), copies: int(1, 9)) {
        // Added: a new tool with none lent. An existing id is Exists.
        outcomes Added;
        examples {
            {} (1, "drill", 2) => Added { tools: [Tool { id: 1, kind: "drill", copies: 2, lent: 0 }] };
            Drill (1, "saw", 1) => Exists;
        }
    }
    contract lend(tool: id) {
        // Lent: one more copy is lent. NoneLeft when every copy is lent. An absent tool is Unknown.
        outcomes Lent, fail NoneLeft;
        examples {
            Drill (1) => Lent { tools: [Tool { id: 1, kind: "drill", copies: 2, lent: 2 }] };
            { tools: [Tool { id: 1, kind: "drill", copies: 2, lent: 2 }] } (1) => NoneLeft;
            Drill (9) => Unknown;
        }
    }
}

unit Cards {
    state cards: Card[16];
    // rule 2: a card holds at most three tools at once.
    invariant all(c in cards: c.holding <= 3);
    fixture Ann = { cards: [Card { id: 7, holding: 1 }] };
    contract issue(card: id) {
        // Issued: a new card holding nothing. An existing id is Exists.
        outcomes Issued;
        examples {
            {} (7) => Issued { cards: [Card { id: 7, holding: 0 }] };
            Ann (7) => Exists;
        }
    }
    contract borrow(card: id) {
        // Borrowed: the card holds one more. AtLimit when it holds three. An absent card is Unknown.
        outcomes Borrowed, fail AtLimit;
        examples {
            Ann (7) => Borrowed { cards: [Card { id: 7, holding: 2 }] };
            { cards: [Card { id: 7, holding: 3 }] } (7) => AtLimit;
            Ann (8) => Unknown;
        }
    }
}

// Both rules are kept by the contracts; the flow is atomic, so a tool with none left leaves the card as it was.
flow borrow(card: id, tool: id) atomic { Cards.borrow(card); Shelf.lend(tool); }

view free(tool: id) = where(t in Shelf.tools: t.id == tool && t.lent < t.copies);

scenario a_saturday {
    Shelf.add(1, "drill", 1) => Added;
    Cards.issue(7) => Issued;
    borrow(7, 1) => Lent;
    free(1) => Value([]);
    borrow(7, 1) => NoneLeft;
    borrow(8, 1) => Unknown;
}

It holds the rows; every unit’s state, its invariant and its fixtures; and every contract as a stub. A stub is a contract with no cases: its header with bounded parameters, the rule it keeps as a one-sentence comment, the line outcomes Lent, fail NoneLeft; that declares its outcomes and which of them are failures, and the examples that pin the rule down. After the units come the flows, the views and the scenarios; a served program’s routes go here too, as the room-booking interface in the appendix shows. Nothing in the file says how any contract does its work.

vishy check --interface checks it as an interface:

vishy check --interface book/programs/interface/writers-lending.vish

ok: 2 row(s), 0 event(s), 0 fn(s), 2 unit(s), 4 contract(s), 3 flow(s)

It refuses an interface that starts doing a writer’s job. Here Cards.borrow has cases where its outcomes should be (the program is book/refusals/interface/writers-body.vish):

book/refusals/interface/writers-body.vish:5:5: error: `Cards.borrow` has cases; an interface declares outcomes, not bodies (`outcomes Ok, fail Full;`)
      contract borrow(card: id) {
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

It also refuses a declared failure without an example that produces it; the Contract anti-patterns page shows that refusal and why it is the rule that pays most.

A part

unit Shelf {
contract add(tool: id, kind: string(32), copies: int(1, 9)) {
    else => Added: tools += [Tool { id: tool, kind: kind, copies: copies, lent: 0 }];
}
contract lend(tool: id) {
    case tools[tool].lent >= tools[tool].copies => fail NoneLeft;
    else => Lent: tools[tool].lent += 1;
}
}

A part is a second declaration of a unit that holds only contract bodies: no state, no rows, no invariant. Its headers must equal the interface’s, and its cases must produce exactly the declared outcomes, no more and no fewer. It needs no examples of its own, because the interface’s examples are appended to it; it may add some.

Why a part can be written alone

The shelf’s writer never sees the cards. Nothing in Shelf may read Cards, and nothing in Cards may read Shelf: the checker refuses a read across units (What Vishy is not shows the refusal). The two meet only in the flow borrow, which is the interface owner’s. So everything a Shelf body can touch is in the interface: its own state, its rows, its rule and its examples. That is the whole of what its writer needs, and the whole of what can make its answer wrong.

What a writer receives

vishy brief book/programs/interface/writers-lending.vish Shelf

prints the brief: the sections of the language reference a part needs, the prelude, the shared declarations with their comments, the world rules that name the unit, and the unit’s block as the interface owner wrote it. Nothing about the other units. It is not reprinted here; most of it is the reference, the same for every unit.

The local check

vishy part book/programs/interface/writers-lending.vish Shelf book/programs/parts/writers-lending.Shelf.vish
vishy part book/programs/interface/writers-lending.vish Cards book/programs/parts/writers-lending.Cards.vish

verify: 5 examples, 0 scenario steps and 1000 sampled checks passed
verify: 5 examples, 0 scenario steps and 1000 sampled checks passed

Each writer checks their part against the interface and then runs their unit alone: the interface’s examples, and five hundred sampled calls per contract against the unit’s invariant. No flows, no scenarios, no world rules: those belong to the whole program. Two writers, two verdicts, and neither waited for the other. When the check fails, it names the contracts to rewrite.

The writer stage

vishy write is a unit owner that is a program: it sends one request per unit to a cheap model, all at once, checks each part with the same local check as it lands, and sends back only the contracts a failed check names, up to three rounds. When every part passes, it assembles and verifies the whole program, and a whole-program failure that names a contract goes back to that unit’s writer. It needs a model endpoint and a key, so this book describes it and does not run it; the appendix gives the handbook’s timings. A unit the stage cannot finish goes to a person, whose part is held to the same vishy part.

Assembly

vishy assemble book/programs/interface/writers-lending.vish book/programs/parts/writers-lending.Shelf.vish book/programs/parts/writers-lending.Cards.vish book/programs/writers-lending.vish

writes the interface and the parts as one program, book/programs/writers-lending.vish: the interface’s text, then each part, which the compiler merges into its unit’s stub. Assembly refuses while any contract is still a stub. The assembled program is checked, run and verified like any other:

scenario a_saturday
  Shelf.add(1, "drill", 1) => Added
  Cards.issue(7) => Issued
  borrow(7, 1) => Lent
  free(1) => Value([])
  borrow(7, 1) => NoneLeft
  borrow(8, 1) => Unknown
  Shelf = Shelf { tools: [Tool { id: 1, kind: "drill", copies: 1, lent: 1 }] }
  Cards = Cards { cards: [Card { id: 7, holding: 1 }] }
6 step(s), all as expected

verify: 10 examples, 6 scenario steps and 8000 sampled checks passed

The scenario’s second borrow shows the flow’s promise: the card was charged, the shelf had none left, and the card is back at one tool because the flow is atomic. Assembly is where the writers’ work first meets; the next chapter is what the verifier does there.

Try

In the cards part, change fail AtLimit to fail TooMany. vishy part refuses: Cards.borrow produces TooMany, which the interface does not declare. The message lists the declared outcomes and the implicit ones, and the check names borrow as the contract to rewrite. Delete the AtLimit case instead, and it refuses again, because AtLimit is declared and no case produces it. A writer cannot invent an answer or drop one; the next chapter shows what that second refusal is worth.