system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Return the number of NFTs owned by a specific address.
/// @dev Throws an error if _owner is the zero address, as it cannot own NFTs.
/// @param _owner Address to retrieve the number of NFTs for.
/// @return The total 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);
