kw ensures

Контекстное слово — контракты функции (§6.7)

Список слов: §1.4

Синтаксис

Contract    = ( "requires" | "ensures" ) Expr ;

Грамматика: Прил. A

Определяется в

• 6.7 Контракты — requires проверяется при входе, ensures — при выходе (result — возвращаемое значение, old(e) — значение e на входе), invariant (§4.2) — посл
• 1.4 Ключевые слова — Зарезервированные (нельзя использовать как имена)

Примеры

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

— 6.7 Контракты

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

contract