Contracts: ensure

● Intermediate3 min

ensure states what the function promises; result is the value it gives back.

type Account {
    owner: String
    balance: Decimal
}

fn withdraw(account: Account, amount: Decimal) -> Account
    require amount > 0
    require amount <= account.balance
    ensure result.balance == account.balance - amount
{
    account with { balance: account.balance - amount }
}

fn main() {
    const after = withdraw(Account(owner: "Asha", balance: 500), 120)
    print(after.balance)
}

kavach run ensure.kav

account.balance in the ensure is the balance before the call: parameters are values and never change, so no special "old value" syntax is needed. An ensure is checked only when the function succeeds.

Found before it runs

When the function gives back a value the compiler knows, and an ensure that compares result with a number is false for it, that is a compile error. This holds for the end of the function, a branch at its end, or a return, even in a branch that may not run: whenever it runs, it panics.

fn clamp_low(x: Int) -> Int
    ensure result >= 0
{
    if x < 0 {
        return -1
    }
    x
}

fn main() {
    print(clamp_low(5))
}

kavach run ensure-known.kav

error: this always breaks `ensure result >= 0` of `clamp_low`: `result` is -1 (spec 7.7)