system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Allow or disallow an "operator" to handle all assets of msg.sender.
/// @dev Emits the ApprovalForAll event upon execution. The contract MUST allow multiple operators to exist for a single owner.
/// @param _operator The address to grant or revoke permission for managing the assets.
/// @param _approved A boolean value indicating whether the operator is approved.

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