Я предпочитаю не увлекаться формализмом, использовать оправдавшие себя шаблоны вроде линейного поиска, но всё же попробую по шагам в википедии доказать вариант инварианта:
Подготовка:CONST
CHAIN_LEN = 2;
CHAIN_BYTE = 0;
ChainLen := 0;
i := 0;
WHILE (i < LEN(a)) & (ChainLen < CHAIN_LEN) DO
IF a[i] = CHAIN_BYTE THEN
INC(ChainLen);
ELSE
ChainLen := 0;
END;
INC(i);
END;GetChainLen - вспомогательная функция, принимающая подмассив и возвращающая длину непрерывной цепочки нулей в нём от конца к началу. Несуществующие индексы игнорируются.
Инвариант:i <= LEN(a) // Из заголовка цикла
ChainLen <= CHAIN_LEN // Из заголовка цикла
GetChainLen(a[i - 2.. i - 1]) = ChainLen1. Доказывается, что выражение инварианта истинно перед началом цикла.
Минимальная длина массива - 0. Максимальная: > 0. i = 0. i <= LEN(a).
ChainLen = 0. CHAIN_LEN = 2. 0 <= 2.
GetChainLen(a[-2..-1]) = 0. 0 <= 2.
2. Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении цикла инвариант будет выполняться.
Переменная i увеличивается на 1 безусловно. Первая часть охраны цикла останавливает повторы при i = LEN(a). Следовательно, i <= LEN(a) верно после каждой итерации.
Переменная ChainLen может расти вверх максимум на 1 за каждую итерацию. Вторая часть охраны цикла гарантирует равенство ChainLen <= CHAIN_LEN. Скачок с 0 до 3 таким образом невозможен.
Если текущий символ не нулевой, то ChainLen обнуляется. GetChainLen анализирует длину цепочки с хвоста и тоже вернёт 0.
Если текущий символ нулевой, то ChainLen растёт на единицу. Точно также поступает при анализе длины и GetChainLen.
Переменная i в конце итерации указывает на следующий за текущим символ. Следовательно,
GetChainLen(a[i - 2.. i - 1]) = ChainLen выполняется.
3. Доказывается, что при истинности инварианта после завершения цикла переменные примут именно те значения, которые требуется получить (это элементарно определяется из выражения инварианта и известных конечных значениях переменных, на которых основывается условие завершения цикла).
Хотим получить ChainLen = 2 при успехе. Тогда i - 2 есть начало цепочки. При неудаче ChainLen < 2, а i = LEN(a).
4. Доказывается (возможно — без применения инварианта), что цикл завершится, то есть условие завершения рано или поздно будет выполнено.
Безусловное увеличение i на 1 после каждой итерации при положительной длине массива гарантирует конечное время выполнения и завершение. Вторая охрана цикла (ChainLen < CHAIN_LEN) гарантирует выход, когда цепочка наберёт критическую длину.
5. Истинность утверждений, доказанных на предыдущих этапах, однозначно свидетельствует о том, что цикл выполнится за конечное время и даст желаемый результат.
Аминь.
Если серьёзно, то схема линейного поиска остаётся в силе. Просто условие окончания не примитивное сравнение элемента с искомым, а длина непрерывной цепочки, которая считается через несложное IF-ELSE.
