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

Returns the account balance of another account with address `_owner`.

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