system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
#### transfer

Transfers `_value` amount of tokens to address `_to`, and MUST fire the `Transfer` event.
The function SHOULD `throw` if the message caller's account balance does not have enough tokens to spend.

*Note* Transfers of 0 values MUST be treated as normal transfers and fire the `Transfer` event.

``` js
function transfer(address _to, uint256 _value) public returns (bool success)
```
assistant
/// @notice postcondition (  __verifier_old_uint(_balances[msg.sender]) - _value == _balances[msg.sender] && msg.sender != ____target  )
/// @notice postcondition ( _balances[____target] == __verifier_old_uint(_balances[____target]) + _value && msg.sender != ____target )
/// @notice emits Transfer
function transfer(address ____target, uint256 _value) public returns (bool success);