Эх, попробовал я таки сделать этот инвариант и понял, что в императивных языках, да ещё и с массивами и циклами, эти ваши инварианты гораздо труднее делать, чем на ФЯ со списками да рекурсиями. По крайней мере, для подобных задачек...
Вот функциональная программа на псевдокоде:
Прим.
list<TYPE> -- это тип "список с элементами типа TYPE", head и tail -- функции, возвращающие, соответственно, первый элемент списка и его хвост.
option<TYPE> -- это тип, который может иметь значение none, что означает "нет значения", или some<X>, что означает "есть значение X типа TYPE"
function find00 (xs: list<int>) : option<int>
function find (xs: list<int>, i: int) : int
begin
{ (список пуст и тогда искомая последовательность не найдена)
или (искомая последовательность находится в первых двух элементах списка)
или (искомая последовательность находится в хвосте списка)
}
if xs = nil then return none
else if head(xs) = 0 and head(tail(xs)) = 0 then return some<i>
else return find (tail(xs), i+1)
end;
begin
return find (xs, 0)
endУсловие завершения для функции find, как видно, такое:
"(список пуст и тогда искомая последовательность не найдена)
или (искомая последовательность находится в первых двух элементах списка)
или (искомая последовательность находится в хвосте списка)"
Теперь вольный перевод этой программы на императивный язык с циклами и массивами:
Прим. Нумерация элементов массива идёт с 1, а не с 0
i := 1;
{ инв: (i > len(a)-1, а значит массив не содержит искомую последовательность)
or (элементы a[i] и a[i+1] содержит искомую последовательность)
or (искомая последовательность находится в части массива c позиции i+1 по len(a)-1)
}
while i < len(a) and (a[i] ≠ 0 or a[i+1] ≠ 0) do
{ инв }
i := i + 1
end;
{ ((i = len(a)) or (a[i] = 0 and a[i+1] = 0)) and инв }Ну и инвариант, соответственно, такой:
"(i > len(a)-1, а значит массив не содержит искомую последовательность)
или (элементы a[i] и a[i+1] содержит искомую последовательность)
или (искомая последовательность находится в части массива c позиции i+1 по len(a)-1)"
Ужасно, должен вам сказать. Я этот ваш инвариант цикла осилил только после того, как описал словами условие завершения рекурсивной функции со списком...
ЗЫ. Опциональные типы option в ML-языках или Maybe в хаскелле гораздо безопаснее, чем null или всякие коды -1 в традиционных императивных языках...
