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

Returns the amount permitted for `_agent` to withdraw from the `_user`'s account.

``` js
function allowance(address _user, address _agent) public view returns (uint256 amountLeft)
```
assistant
/// @notice postcondition _allowed[_owner][_spender] == remaining
function allowance(address _owner, address _spender) public view returns (uint256 remaining);