Доказательство инварианта
Доказательство инварианта — это проверка того, что выбранное свойство истинно перед началом цикла и сохраняется после каждой его итерации. Если цикл завершился, инвариант помогает сделать вывод о результате алгоритма.
Инвариант цикла — свойство, которое не изменяется в важном для доказательства смысле во время работы цикла. Подробно понятие разобрано на странице инвариант цикла. Доказательство обычно проводят в таком порядке:
- До цикла. Проверяют начальную истинность инварианта: он должен выполняться до первой проверки условия или перед первой итерацией.
- После итерации. Предполагают, что инвариант был верен перед итерацией, и показывают, что после выполнения команд он снова верен.
- При завершении. Учитывают, что условие продолжения стало ложным. Вместе с инвариантом это должно давать требуемый результат.
В цикле просматривают элементы массива и хранят переменную \(m\). Инвариант: после обработки первых \(i\) элементов \(m\) равен их максимальному значению. До цикла обработан один первый элемент, поэтому свойство верно. После итерации новый элемент сравнивают с \(m\) и при необходимости заменяют \(m\) — максимум обработанной части сохраняется. При завершении обработаны все элементы, значит \(m\) — максимум всего массива.
Инвариант не обязан сохранять неизменным значение переменной или состояние всей программы. Сохраняется именно сформулированное свойство. Кроме того, инвариант сам по себе не доказывает остановку цикла: отдельно проверяют достижение условия завершения. После этой страницы можно перейти к применению инварианта цикла.
Что нужно доказать на втором шаге?
Главное
- Проверяют начальную истинность, сохранение после итерации и вывод при завершении.
- Инвариант описывает свойство, а не обязательно неизменное значение переменной.
- Для полной корректности отдельно учитывают, что цикл завершится.