system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Assign or modify the approved address for an NFT.
/// @dev A zero address input will revoke the current approval.
/// Only the NFT owner or an authorized operator can perform this action.
/// @param _approved Address to grant approval to manage the NFT.
/// @param _tokenId NFT identifier for which approval is being granted.

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