system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Authorize or revoke permission for a third party ("operator") to manage all assets owned by msg.sender.
/// @dev This function triggers the ApprovalForAll event. The contract MUST support having multiple operators for each owner.
/// @param _operator The address to grant or revoke management privileges.
/// @param _approved True to approve the operator, false to remove approval.

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