system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Grant or deny permission for an operator to handle all assets owned by msg.sender.
/// @dev Emits the ApprovalForAll event. Multiple operators can coexist for any given owner.
/// @param _operator Address to be approved or revoked as an operator.
/// @param _approved True indicates approval; false indicates revocation.

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