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

* Moves _value tokens to target.
* Must revert if the sender’s balance is lower than the specified amount.

Observations:
* Transfers of 0 tokens should trigger the `Transfer` event as usual.

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