system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Assign or remove the ability of an "operator" to manage all assets of msg.sender.
/// @dev Emits the ApprovalForAll event. Each owner may approve multiple operators.
/// @param _operator The address that will gain or lose authorization as an operator.
/// @param _approved Boolean to set approval as true or false.

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