system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Set or revoke the approval status of an operator for all assets of msg.sender.
/// @dev Triggers the ApprovalForAll event upon modification. Multiple operators per owner are allowed.
/// @param _operator Address to authorize or revoke authorization for asset management.
/// @param _approved Boolean value: true for approval, false to revoke.

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