system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Find out how many NFTs belong to a given address.
/// @dev Reverts if _owner is the zero address, as it is not valid for NFT ownership.
/// @param _owner Address for which the NFT count is requested.
/// @return The total count of NFTs owned by _owner.

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