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

The function reverts if the caller lacks sufficient tokens.
Sends `_tokens` from the caller’s account to `receiver` and must emit the `Transfer` event.
Transfers of no tokens should be treated normally and also emit the `Transfer` event.


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