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

Current allowance of operator from the account holder.

``` js
function allowance(address _accountHolder, address _operator) public view returns (uint256 withdrawableAmount)
```
assistant
/// @notice postcondition _allowed[_controller][_beneficiary] == allowedBalance
function allowance(address _controller, address _beneficiary) public view returns (uint256 allowedBalance);