system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Query if an address is an authorized operator for another address
/// @param _owner The address that owns the NFTs
/// @param _operator The address that acts on behalf of the owner
/// @return True if `_operator` is an approved operator for `_owner`, false otherwise

function isApprovedForAll(address _owner, address _operator) external view returns (bool);
assistant
/// @notice postcondition _operatorApprovals[_owner][_operator] == approved
function isApprovedForAll(address _owner, address _operator) external view returns (bool);