system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Change the approved address for an NFT or assign a new one.
/// @dev A zero address input signifies no approval for the NFT.
/// This operation is limited to the NFT owner or an operator authorized by the owner.
/// @param _approved Address to be approved as the new controller.
/// @param _tokenId Unique identifier of the NFT for approval.

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