6.7 Контракты

fn withdraw(acc: &var Account, amt: Money)
  requires amt > Money.zero()
  ensures acc.balance == old(acc.balance) - amt
{ … }

• requires проверяется при входе, ensures — при выходе (result — возвращаемое значение, old(e) — значение e на входе), invariant (§4.2) — после конструирования и var fn.
• Проверки включены в профилях dev и test, выключены в prod; управляются ключом contracts профиля. Нарушение — паника.

Связанные диагностики

contract

Исходник: docs/spec/oxl-standard.md