I'm no expert on formal verification and @istvan's answer is helpful. Indeed, one can transfer the coins to an address one doesn't control (the usual idea), but there is no guarantee anyone or anything has sufficient control to ever spend them. Alice sent to Bob. Bob lost his key. Poor Bob.
Solidity has some new verbs to replace the old throw
and help automated verification systems assess the correctness of the code: require
, assert
and 'revert'. In summary, use require
to concentrate on inputs and assert
to verify normal conditions (an assert
should never be false
). revert
is still available as an approximate replacement for throw
.
Details: Difference between require and assert and the difference between revert and throw
A quick reinterpretation of the example code might look something like:
contract Token {
mapping(address => uint) balances;
function transfer(address from, address to, uint amount) {
require(balances[from] >= amount);
uint initialSum = balances[from] + balances[to];
balances[from] -= amount;
// update, safeAdd idea
require(balances[to] < balances[to] + amount);
balances[to] += amount
uint newSum = balances[from] + balances[to];
assert(newSum == initialSum);
}
}
}
Now a verification suite can explore possibilities. It can try a range of inputs and cases that pass the require
and see if there is ever any scenario in which that assert
fails. If the assert
can fail it would be treated as a discovered defect.
Hope it helps.
Update: @karthikeyan has a good point about safe math, so added a little overflow check.