system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Calculate the total NFTs owned by a particular address.
/// @dev Any queries for the zero address are invalid and will result in an error.
/// @param _owner The address to query for its NFT balance.
/// @return The number of NFTs _owner owns, or zero if none exist.

function balanceOf(address _owner) external view returns (uint256);
assistant
/// @notice postcondition _ownedTokensCount[_owner] == balance
function balanceOf(address _owner) public view returns (uint256 balance);
