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


This function sends `val` tokens to the address `t` and must trigger the `Transfer` event.
It will fail (`throw`) if the sender's account doesn’t have enough tokens.

Note: Sending 0 tokens is allowed and will still trigger the `Transfer` event.

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