Contracts
Also known as: precondition postcondition assert invariant require ensure design by contract validation
● Intermediate5 minBefore this: Signatures, PanicsSpec 7
A contract states in one line what a function needs and what it promises, and Kavach checks it.
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)
}The program ran and printed:
kavach run ensure.kav
380require: what must be true when the function is called. If not, the caller has a bug.ensure: what the function promises about itsresult.invariant: what is always true of a type's values.example: one real call and its answer.
When someone else, or an AI, writes the body, you review the contract: it is short, and Kavach checks that the body keeps it.