system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Count all NFTs assigned to an owner
/// @dev NFTs assigned to the zero address are considered invalid, and this
///  function throws for queries about the zero address.
/// @param _owner An address for whom to query the balance
/// @return The number of NFTs owned by `_owner`, possibly zero

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