State, contracts and outcomes

A unit is a piece of state and the only operations that may change it. This chapter is about those three words: state, the contracts that change it, and the outcomes a contract names.

unit Counter {
    state n: int = 0;
    state bumps: int = 0;
    contract bump() => Bumped: n += 1, bumps += 1;
    contract add(k: int(1, 10)) -> int {
        else => Added(n + k): n += k, bumps += 1;
    }
    contract reset() => Reset: n := 0;
    contract read() -> int => Value(n);
}
scenario a_morning {
    Counter.bump() => Bumped;
    Counter.add(5) => Added(6);
    Counter.reset() => Reset;
    Counter.read() => Value(0);
}

State

state n: int = 0; declares a field the unit owns, its type, and its starting value. A unit may have several fields; here n is the count and bumps counts how many times it was changed. Nothing outside the unit can read or write either. That sentence is the first of the language’s two removals, and it holds for every unit in every program.

Contracts

A contract is the unit’s operation. It has a header, add(k: int(1, 10)) -> int, and a body of cases. A case is a guard, an outcome, and the deltas that follow the colon: what changes. else is the case with no guard. When a contract has one case and no guard, the body collapses to a single line: contract bump() => Bumped: n += 1, bumps += 1; is the same as writing an else case in braces.

The deltas name exactly what changes and nothing else changes: n += 1, bumps += 1 adds one to both fields; n := 0 sets one field and leaves bumps alone. Every right-hand side reads the state as it was before the call, so Added(n + k) carries the new total while n += k writes it, and the two agree.

The parameter type int(1, 10) is a bound: add accepts one to ten and nothing else. A bound is enforced in three places at once: an example with an out-of-range argument is refused by the checker, the verifier only samples arguments inside it, and a served application refuses a request outside it. Bounds are how a rule about a quantity is written once.

Outcomes

Every case names an outcome: Bumped, Added, Reset, Value. An outcome is the contract’s answer, and the name is part of the program’s meaning: a caller switches on it, a scenario asserts it, a client library gets a type for it. Outcomes are of two kinds. A plain outcome, Bumped, says the case applied and the deltas happened. A carried outcome, Added(n + k) or Value(n), brings a value with it; the contract’s header then says the value’s type after ->. The next chapter adds the third kind, a failure, which changes nothing.

Two rules about names. The same outcome name means the same thing everywhere in a program: if Added carries an int here, no other contract may use Added as a failure or with another type. And the names are yours: the language reserves only the four outcomes it produces itself, which the chapter on rows introduces.

The scenario

scenario a_morning calls the contracts in order and states each answer. vishy run executes it:

scenario a_morning
  Counter.bump() => Bumped
  Counter.add(5) => Added(6)
  Counter.reset() => Reset
  Counter.read() => Value(0)
  Counter = Counter { n: 0, bumps: 2 }
4 step(s), all as expected

The final state shows both fields: n is back to zero after reset, and bumps is two, because reset did not name it in its deltas and so did not change it.

What the verifier does with no rules

verify: 0 examples, 4 scenario steps and 8000 sampled checks passed

Eight thousand sampled calls across the four contracts, from random states and from states reached by earlier calls: a random n, a random bumps, a random k inside its bound. Nothing in this program says what must be true, so the verifier can only confirm that every call ended in a declared outcome. The next chapter gives it something to look for.

Try

Change add’s parameter to k: int and its line to Added(n + k): n += k;. The program still checks, runs and verifies. Now the count can go down as well as up, and nothing in the program says it may not. Keep that in mind for the next chapter, where a rule is written and the verifier finds the call that breaks it.

Keyboard shortcuts