v0.3.4
This release includes both new language features as well as bug fixes.
New Language Features
Support for user-defined functions (#15). These are loop-free functions defined at the contract level (in the contract doc strings) that are available for all properties in that contract to refer to.
For example consider a toy 'wallet' contract, that keeps internal track of the balances of several tokens per user, in its _balances field:
contract Wallet {
mapping(address => address => uint) _balances;
function transferFrom(address from, address to, address token, uint amount) public {
...
}
}
One might want to check that after transferFrom, the internal balance equals the 'real' balance in each token. To save on writing, we can add define our own function for getting the real balance and use it as follows:
/// define realBalance(address user, address token) uint = IERC20(token).balanceOf(user);
contract Wallet {
mapping(address => address => uint) _balances;
/// if_succeeds {:msg "Internal balance matches real balance"}
/// realBalance(from, token) == _balances[from][token] &&
/// realBalance(to, token) == _balances[to][token];
function transfer(address from, address to, address token, uint amount) public {
...
}
}