5.8. Naming a failure with summary🔗

An assert, a requires, or an ensures may carry summary "...", which is attached to the diagnostic reported when that obligation fails. It is the difference between a failure that identifies itself and one the reader has to decode from a line number, so it is worth writing on any clause a front end generates on a user's behalf — the summary can name the source-language reason rather than the Laurel one.

procedure indexed(xs: Sequence<int>, i: int): int
  requires 0 <= i summary "index must not be negative"
  requires i < seqLength(xs) summary "index must be within bounds"
{
  return seqSelect(xs, i)
};