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

Gets the balance of the `_user` account in terms of total tokens owned.

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