system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Approves an address to control a specific NFT.
/// @dev Use the zero address to remove any existing approval for the NFT.
/// The caller must either be the NFT's current owner or an operator authorized by the owner.
/// @param _approved The address that will be granted approval.
/// @param _tokenId The identifier of the NFT to approve.

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