system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Designate or update the approved manager for a specific NFT.
/// @dev Clearing approval can be achieved by providing the zero address.
/// This function requires the caller to either own the NFT or be an authorized operator.
/// @param _approved The address to grant management authority over the NFT.
/// @param _tokenId The identifier of the NFT in question.

function approve(address _approved, uint256 _tokenId) external payable;
assistant
/// @notice postcondition _tokenApprovals[_tokenId] == _approved
function approve(address _approved, uint256 _tokenId) external;