system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Grant or withdraw management rights to an "operator" for all of the assets owned by msg.sender.
/// @dev When called, it emits the ApprovalForAll event. The contract MUST support multiple operators for the same owner.
/// @param _operator Address being approved or revoked for management privileges.
/// @param _approved True for granting, false for revoking.

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