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

Returns the token balance for targetAddress. Useful for getting the total amount held by a specific account.

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