Как написать инвариант цикла в бинарном поиске

Сколько я не видел материалов по бинарному поиску - все описывают простейшую форму бинарного поиска в таком виде:

public int Search(int[] nums, int target)
{
    var left = 0;
    var right = nums.Length - 1;
    
    while (left <= right)
    {
        var mid = left + (right - left)/2;
        
        if(nums[mid] == target)
            return mid;
        
        if(nums[mid] < target)
            left = mid + 1;
        else
            right = mid - 1;
    }

    return -1;
}

И я всё время сколько пишу бинарные поиски задумываюсь о том, как мне логически объяснить почему в цикле while стоит условие left <= right, а не left < right? Каждый раз сижу и задумываюсь, какой знак поставить, а главное -- почему так?

Как ни странно, но нигде нет объяснения, возможно это настолько очевидно, что даже пояснять не надо? Прямо говоря, мне не очень хочется запоминать этот факт as is, а хочется понять. Есть ли какое-то объяснение, как лучше понять механику работы этого условия?


Ответы (1 шт):

Автор решения: Pak Uula

В принципе можно использовать строгое неравенство, но в этом случае необходимо проверить после цикла, что элемент nums[l] равен target.

Пример - массив из двух элементов [0, 2], ищем target = 1.

В первой итерации l = 0, r = 1, mid = 0.

Тогда nums[mid] == 0, то есть nums[mid] < target. Следовательно, l становится равным 1. Цикл while (l<r) { ... } завершается. Но l нельзя вернуть, так как nums[1] != target. Поэтому перед выходом надо проверить, что лежит в массиве по индексу 1.

public int Search(int[] nums, int target)
{
    // UPDATE добавлена обработка пустого массива
    if (0 == nums.Length) { return -1; }

    var left = 0;
    var right = nums.Length - 1;
    
    while (left < right)
    {
        var mid = left + (right - left)/2;
        
        if(nums[mid] == target)
            return mid;
        
        if(nums[mid] < target)
            left = mid + 1;
        else
            right = mid - 1;
    }

    return (nums[left] == target)? left : -1;
}
→ Ссылка