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

Transfers a given value to a beneficiary address, ensuring the `Transfer` event is fired.
The function should revert if the caller doesn’t have enough tokens to cover the amount.

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