Skip to content
Kavachकवच

Contracts: invariant

● Intermediate3 min

invariant states what is always true of a type. A value that breaks it can't exist.

type Account {
    owner: String
    balance: Decimal

    invariant balance >= 0
}

fn main() {
    let a = Account(owner: "Asha", balance: 100)
    a.balance -= 30
    print(a.balance)
    a.balance -= 200
    print(a.balance)
}

The program ran, then stopped with a panic:

kavach run invariant.kav

70panic: contract failed: invariant balance >= 0
invariant.kav: Kavach code, then what running it prints

The invariant is checked every time an Account is made or changed: the first change is fine, the second would make the balance negative.