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

- This function outputs the token balance for any address provided, such as `addr_`.
- It is read-only and doesn't alter the state.

``` js
function balanceOf(address addr_) public view returns (uint256 balance)
```
assistant
/// @notice postcondition balance == _balances[addr_]
function balanceOf(address addr_) public view returns (uint256 balance);