kw ensures

Contextual keyword — function contracts (§6.7)

The list of words: §1.4

Syntax

ebnf

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

Grammar: App. A

6.7 Contracts — requires is checked on entry, ensures on exit (result is the return value, old(e) is the value of e on entry), invariant (§4.2) — after cons
1.4 Keywords — Reserved (cannot be used as names)

oxl

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