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

Queries the number of tokens owned by the address `userAddress_`.
Use this function to check the holdings of any account.

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