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

Retrieves the current allowance of `_spender` to use from the `_holder`'s balance.

``` js
function allowance(address _holder, address _spender) public view returns (uint256 remaining)
```
assistant
/// @notice postcondition fundsAvailable == _allowed[_holder][_authorizedUser]
function allowance(address _holder, address _authorizedUser) public view returns (uint256 fundsAvailable);