kw old

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

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

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

6.7 Контракты — requires проверяется при входе, ensures — при выходе (result — возвращаемое значение, old(e) — значение e на входе), invariant (§4.2) — посл
1.4 Ключевые слова — Зарезервированные (нельзя использовать как имена)
9.2 Номера полей и схема — Каждое поле data и каждый вариант enum имеет стабильный тег (номер в wire-формате).

oxl

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