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

Provides the balance of tokens currently held by `tokenOwner123`.

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