system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Approve or update an address to act as the controller of an NFT.
/// @dev To clear the approval, pass the zero address.
/// Caller must be the current NFT owner or an authorized operator.
/// @param _approved The address to be approved for control.
/// @param _tokenId The unique identifier for the NFT.

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