6.7 Contracts

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

• 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 construction and after var fn.
• Checks are enabled in the dev and test profiles and disabled in prod; they are controlled by the profile key contracts. A violation is a panic.

Related diagnostics

contract

Source: docs/spec/oxl-standard.en.md