system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Set or update the approved address for a specific NFT.
/// @dev The approval can be cleared by passing the zero address.
/// The caller must be either the NFT's owner or an operator designated by the owner.
/// @param _approved The address to set as the approved controller.
/// @param _tokenId The NFT identifier.

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