system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Check which address is approved to manage a given NFT.
/// @dev The function will throw if _tokenId does not refer to a valid NFT.
/// @param _tokenId Identifier of the NFT for which approval is being queried.
/// @return Address approved to manage the NFT, or zero if no approval exists.

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);