system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Grant or change the approved controller for a given NFT.
/// @dev Passing the zero address revokes any current approval for the NFT.
/// This function will fail unless the caller owns the NFT or is an authorized operator for the owner.
/// @param _approved The address to authorize for managing the NFT.
/// @param _tokenId The unique identifier of the NFT.

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