system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Approve or disapprove an operator to manage all of msg.sender's assets.
/// @dev This emits the ApprovalForAll event and permits multiple operators for one owner.
/// @param _operator The address for which approval is being granted or removed.
/// @param _approved A boolean specifying whether to approve or revoke access.

function setApprovalForAll(address _operator, bool _approved) external;
assistant
/// @notice postcondition _operatorApprovals[msg.sender][_operator] == _approved
function setApprovalForAll(address _operator, bool _approved) external;