system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Toggle permission for an "operator" to oversee all assets of msg.sender.
/// @dev Triggers the ApprovalForAll event and allows the owner to assign multiple operators.
/// @param _operator The address to be approved or disapproved for managing assets.
/// @param _approved Boolean indicating the approval status.

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