system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Fetch the NFT balance of a specified address.
/// @dev The zero address is not allowed, and the function will revert if queried.
/// @param _owner Address to retrieve the NFT count for.
/// @return Number of NFTs owned by _owner, including zero if none are held.

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