Capabilities and contracts

Capabilities and contracts

Declare an operation's inputs, result and promised behavior. Use capability inside a concept-like declaration and function at the top level.

Capability syntax

A capability has a name and parenthesized parameters. Each parameter has a name and type. Add returns for the result and fails with for declared exceptional outcomes. A contract body can contain requires, ensures and promises.

The StoreGame public save example is complete. Listing save in public exposes it. The declaration alone does not.

Parameters and defaults

main.expec

function formatLabel(
  title: Text,
  suffix: Text = title,
) returns Text {
  promises "Format the supplied title and suffix."
}
examples {
  example "use the default suffix": formatLabel("Dune") => satisfies "A label for Dune."
}

Calls supply positional arguments. Omitted arguments need declared defaults. Required parameters cannot follow defaulted parameters. A parameter default may refer to an earlier parameter, but not itself or a later one. An explicitly supplied wrong type remains wrong even when a default exists.

Returns and Nothing

returns Number promises a numeric result. returns Nothing explicitly promises no result value. Omitting returns leaves the result unspecified; it does not mean Nothing and cannot establish a value for later use. A call used only for its effect can still be described without a result, but prefer an explicit result when you know it.

A capability or function body is a contract body, not an implementation body. You cannot put return, loops or arbitrary application code there. Reusable test helper bodies are a different construct.

Preconditions and postconditions

main.expec

function multiply(a: Number, b: Number) returns Number {
  requires a >= 0 and b >= 0
  ensures result >= 0
  promises "Return the product of the inputs."
}

requires describes a Boolean precondition. ensures describes a Boolean postcondition. In ensures, result refers to the declared result value. It is unavailable as that contextual value in a precondition, a default, or a callable returning Nothing.

Parameters remain available in conditions. Avoid declaring a parameter named result when it would conflict with the contextual postcondition result. Outside that special context, result can be an ordinary authored name.

Checking verifies types and references. It does not prove multiply actually calculates a product or automatically inject runtime checks into every generated application method.

Human-readable promises

promises "…" records prose about the operation. Multiple promises remain distinct. They communicate intent and become visible verification/implementation obligations where relevant; natural language is not interpreted as executable code.

For concrete expected values use examples. For a prose example expectation use satisfies "…".

Related: Concepts and construction · Types · Domain errors