system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Discover the owner address of a specific NFT identified by _tokenId.
/// @dev If _tokenId is assigned to the zero address, the function will throw as it is invalid.
/// @param _tokenId The identifier for the NFT being queried.
/// @return The address currently owning the specified NFT.

function ownerOf(uint256 _tokenId) external view returns (address);
assistant
/// @notice postcondition _tokenOwner[_tokenId] == _owner
/// @notice postcondition  _owner !=  address(0)
function ownerOf(uint256 _tokenId) public view returns (address owner);