system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Check the total number of NFTs linked to an address.
/// @dev This function does not support queries for the zero address and will throw in such cases.
/// @param _owner The address being checked for NFT ownership.
/// @return The NFT count for _owner, possibly zero if none are owned.

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