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

Get the amount that `_spender` can still spend in the behalf of `_account`.

``` js
function allowance(address _account, address _spender) public view returns (uint256 leftToWithdraw)
```
assistant
/// @notice postcondition _allowed[_sender][_receiver] == approvedAmount
function allowance(address _sender, address _receiver) public view returns (uint256 approvedAmount);