Account3

type money

function (X:money + Y:money) : money

object account = {

    individual balance : money
    init balance = 0

    action deposit(x:money) = {
    balance := balance + x
    }

    action withdraw(x:money) = {
    balance := balance - x
    }

    action get_balance returns(x:money) = {
    x := balance
    }

    object spec = {
    before deposit {
        assert balance + x >= balance
    }
    before withdraw {
        assert x <= balance
    }
    }

}


import action ask returns (x:money)

export action ask_and_check_balance returns(ok:bool) = {
    ok := ask <= account.get_balance
}

export account.deposit
export account.withdraw
export account.get_balance

interpret money -> bv[16]