system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Get the approved address for a single NFT
/// @dev Throws if `_tokenId` is not a valid NFT.
/// @param _tokenId The NFT to find the approved address for
/// @return The approved address for this NFT, or the zero address if there is none

function getApproved(uint256 _tokenId) external view returns (address);
assistant
/// @notice postcondition _tokenOwner[tokenId] != address(0)
/// @notice postcondition _tokenApprovals[tokenId] == approved
function getApproved(uint256 _tokenId) external view returns (address approved);