4.8. Procedures, outputs, and calls🔗

A procedure has three output styles. It may have none, one anonymous output, or named outputs:

procedure log(x: int) { assert x == x };

procedure addOne(x: int): int
{
  return x + 1
};

procedure quotientAndRemainder(a: int, b: int)
  returns (q: int, r: int)
  requires b != 0
  opaque
  ensures a == q * b + r
{
  q := a / b;
  r := a % b
};

The short : T form names the output $result, which is the one exception to the reserved leading $ (see Reserved names): you may write returns ($result: T) explicitly and refer to it in a contract. Prefer returns (r: T) with a name of your own whenever a contract needs the result. return e is valid only when there is exactly one output; a multi-output procedure assigns its named outputs and uses a bare return for an early exit, which leaves the outputs at whatever they were last assigned.

An input and an output that share a name form an inout parameter — the standard way to model a procedure that updates its argument:

procedure bump(x: int) returns (x: int)
  opaque
  ensures x == old(x) + 1
{
  x := x + 1
};

Top-level procedures may share a name when their parameter signatures do not overlap; resolution picks the unique overload the argument types accept, and both no match and several matches are errors. external procedures cannot be overloaded.

4.8.1. Bodiless and external procedures🔗

A procedure may be declared without a body, in which case its contract is all there is. This is the right way to model an operation whose implementation is outside the program — a boundary call, or a stub standing in for code not yet translated. Its outputs are arbitrary subject to its postconditions:

procedure boundary(x: int) returns (r: int)
  opaque
  ensures r >= x;

external is different: it declares an operation supplied by the Core environment itself. The declaration exists so Laurel can resolve calls to it, and is then dropped, with each call becoming an application of a Core operator. Use exactly one output.

procedure hostPrimitive(x: int): int external;

Do not reach for external when what you want is an unconstrained value — that is a bodiless opaque procedure. The distinction between a transparent procedure, whose body callers may reason through, and an opaque one, whose contract is all callers see, is a verification concern and is covered under Postconditions.