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

Gets the allowed balance still available for `_beneficiary` to spend in the name of `_controller`.

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