Инвариант цикла

Инвариант цикла

Инвариант цикла

Программисты часто составляют циклы, как правило, чтобы достичь какой-то конкретной цели: найти элемент с заданными свойствами, выполнить сортировку и т. п. Но как убедиться в том, что цель будет достигнута, не выполняя цикл непосредственно? В этом нам поможет инвариант цикла.

Инвариант цикла — это утверждение, относящееся к переменным программы, которое остается истинным в начале и в конце выполнения каждой итерации цикла.

…// Инвариант цикла должен быть истинным здесьwhile ( Условие_выполнения_цикла ) { // начало тела цикла … // конец тела цикла // Инвариант цикла должен быть истинным здесь}…

Рассмотрим использование инварианта цикла на примере поиска индекса наименьшего элемента в целочисленном массиве.

Пусть имеется массив a, состоящий из n элементов. Введем переменную TemporarySmallest (индекс элемента, в данный момент являющегося наименьшим) и положим ее равной 0 перед началом проверки.

Далее, будем сравнивать a[TemporarySmallest] последовательно с a[1], a[2], …, a[n-1]. Если окажется, что a[TemporarySmallest] больше какого-либо из a[k], то обновим значение TemporarySmallest.

Обозначим переменой nextToCheck индекс элемента, подлежащего проверке.

Инвариант цикла будет выглядеть так:

  1. TemporarySmallest находится внутри [0,nextToCheck),
  2. и для всех k из [0,nextToCheck) выполняется A[k] >= A[TemporarySmallest].
[a,b) означает: все целые числа, находящиеся на промежутке от a до b, включая a, но не включая b.

Другими словами: наименьший элемент массива с известным индексом TemporarySmallest находится внутри исследованного промежутка [0,nextToCheck). Это утверждение должно оставаться истинным в начале и в конце каждой итерации.

Инициализируем переменные, входящие в инвариант, так, чтобы он был истинным до начала выполнения цикла:

nextToCheck = 1;TemporarySmallest = 0;

— индекс наименьшего элемента равен 0, и это единственный элемент в исследованном промежутке [0,1). Пока инвариант сохраняется.

На каждом шаге цикла значение nextToCheck увеличивается на 1, и, при необходимости, изменяется TemporarySmallest:

if ( a[TemporarySmallest] > a[nextToCheck] ) { TemporarySmallest = nextToCheck ; } nextToCheck++ ;

— так, чтобы инвариант цикла оставался истинным в конце каждой итерации. Следовательно, и по окончании цикла инвариант сохранится — наименьший элемент массива с известным индексом TemporarySmallest будет находиться внутри исследованного промежутка [0,nextToCheck).

Условием окончания цикла является отсутствие в массиве a элементов, подлежащих проверке: nextToCheck == n. Таким образом, сохранение инварианта цикла гарантирует нам, что по окончании цикла (исчерпании элементов, подлежащих проверке) будет найден индекс наименьшего элемента TemporarySmallest — достигнута цель цикла. Это можно записать как

Инвариант цикла && Условие_окончания_цикла => Цель цикла

Вместо условия окончания можно использовать условие выполнения цикла. В нашем случае это: nextToCheck < n (пока есть элементы для проверки). Как только оно будет нарушено (станет ложным), выполнение цикла прекратится

Инвариант цикла && !(Условие_выполнения_цикла) => Цель цикла

Таким образом, подобрав инвариант цикла и обеспечив его сохранение, мы можем гарантировать достижение цели, не выполняя сам цикл.

Заметим, что использование инварианта цикла позволяет рассматривать итерации по отдельности, поскольку каждая из них начинается с одного и того же состояния — истинности инварианта цикла, и, в этом смысле, не содержит «следов» прошлых итераций. В результате, рассуждения о том, правильно ли работает цикл, сводятся к проверке того, восстанавливается ли истинность инварианта цикла в конце итерации.

Вопросы для самопроверки при составлении циклов:

  • Является ли инвариант цикла истинным до начала цикла (инициализированы ли должным образом nextToCheck и TemporarySmallest)?
  • Для произвольной итерации: является ли инвариант цикла истинным на входе в тело цикла, и по выходе из него?
  • Происходит ли движение по направлению к окончанию выполнения цикла (инкрементируется ли индекс nextToCheck в теле цикла)?
  • Приводит ли сохранение инварианта цикла и условия окончания цикла к достижению цели?

При составлении циклов может оказаться удобным понятие области неопределенности, используемое в вычислительных методах математики.

Область изменения параметров задачи (в нашем примере: [0,n)) можно разделить на две части: исследованную область (для которой найден TemporarySmallest: [0,nextToCheck)) и область неопределенности ([nextToCheck,n)).

Необходимо составлять цикл так, чтобы на каждой итерации область неопределенности сокращалась.

Вернемся к нашему примеру. В начале первой итерации исследованная область представляла собой единственную точку 0, а область неопределенности составляла [1,n). На втором шаге область неопределенности сократилась до [2,n), на третьем — до [3,n) и т. д., пока, наконец, не превратилась в пустое множество, не содержащее точек.

Рассмотрим еще один пример — сортировку выбором по убыванию. Пусть, нужно отсортировать массив a из n целых чисел. Найдем наименьший элемент и поместим его в конец массива, на позицию n-1.

Затем среди оставшихся элементов вновь выберем наименьший и поместим его на позицию n-2 и т. д.

На i-й итерации отсортированные элементы будут занимать позиции от i до n-1, а оставшиеся невыбранными — от 0 to i-1.

Для поиска наименьшего элемента используем функцию FindMin(int a[], int n), возвращающую индекс наименьшего элемента и написанную на основе рассмотренного выше примера. Введем переменную numSorted, обозначающую количество отсортированных элементов массива.

Инвариант цикла будет таким:

  1. numSorted наименьших элементов массива отсортированы в убывающем порядке на промежутке [n-numSorted,n),
  2. оставшиеся элементы массива находятся на промежутке [0,n-numSorted).

Непосредственно перед циклом инициализируем значение numSorted:

numSorted = 0;

что делает инвариант цикла истинным.

На каждой итерации количество numSorted увеличивается на единицу. Чтобы этого достичь, выбирается наименьший среди первых [0,n-numSorted) неотсортированных элементов, и меняется местами (с помощью функции swap()) c элементом n-numSorted

i = findMinumum(A,n-numSorted);numSorted++;swap(A, i, n-numSorted);

Таким образом, отсортированный «хвост» массива всякий раз удлиняется на один элемент, а неотсортированная «голова» уменьшается.

Цикл оканчивается по достижении numSorted == n.

Вирт Н. Алгоритмы + структуры данных = программы

Все есть на Library Genesis.

Источник: http://dkhramov.dp.ua/Comp.LoopInvariant

Алгоритмы (теория/практика): Часть 5. Корректность алгоритмов

Инвариант цикла

Привет! Давайте сегодня рассмотрим такую тему, как корректность алгоритмов. Я не хочу сейчас вводить новые понятия, поэтому настоящая тема будет базироваться только на том, что было описано до этого. Вероятно, когда статей будет больше, их порядок поменяется и некоторые статьи будут расширены. Вся история изменений будет в самом низу.

Как мы можем судить о том, что наш алгоритм действительно корректный? Корректный алгоритм – это алгоритм, способный для любых входных данных выдать результат в виде корректных выходных данных. Например, если мы рассматриваем алгоритм поиска, то результатом его работы должен быть индекс найденного элемента, либо число -1.

Для проверки корректности алгоритма существует несколько способов.

Инвариант цикла

Если речь идёт об циклических алгоритмах, то на помощь приходит инвариант цикла. Это некоторое условие, которое должно обязательно обладать тремя свойствами:

  1. Инициализация: инвариант должен быть справедливым перед первой итерацией.
  2. Сохранение: инвариант должен быть справедливым после каждой итерации.
  3. Завершение: инвариант справедлив после завершения цикла.

Для проверки корректности циклического алгоритма мы должны найти такое условие, которое будет справедливо перед началом цикла, в каждом прохождении цикла и после его завершения. И если такое условие будет найдено, но мы сможем сделать вывод о правильности нашего разрабатываемого алгоритма.

Разумеется, что инвариант должен быть связан с переменными, которые изменяются в теле цикла. То есть условие \(1\lt2\), которое, очевидно, будет соблюдаться во всех трёх случаях, не особо нам поможет.

Нахождение инварианта не всегда является очевидной задачей, поэтому давайте попробуем на примере разобраться с тем, что нужно сделать.

В прошлой статье я показал алгоритм линейного поиска – довольно примитивный, но для нашей задачи он идеально подойдет, так как это типичный пример циклического алгоритма. Для тех, кто забыл, как он выглядит, вот его код:

int linear_search(int arr[], int n, int target) { for (int i = 0; i < n; i++) { if (arr[i] == target) { return i; } } return -1; }

С этим кодом связана определенная проблема, которая заключается в невозможности проверки условия после выполнения цикла в случае, если искомое значение было найдено. Поэтому давайте его перепишем следующим образом:

int linear_search2(int arr[], int n, int target) { int i = 0; while (i < n && arr[i] != target) { i++; } return i != n ? i : -1; }

Замечание: сначала инициализируется переменная-счетчик. Цикл while содержит в себе два условия и, если они оба выполняются, значит мы еще не достигли конца массива и элемент всё еще не найден, а значит нужно увеличить счетчик на единицу и повторить еще раз.

Рано или поздно одно из условий будет будет нарушено и цикл завершится. После чего мы возвращаем значение, если мы его нашли, либо возвращаем -1, если нет. Это делается при помощи проверки условия i != n.

Если переменная-счетчик равна длине массива, то тело цикла while было выполнено n раз, а значит мы проверили весь массив.

В противном случае, несколько итераций не были выполнены, а это возможно только в случае успешного нахождения позиции искомого значения.

Теперь давайте найдем инвариант цикла. Внимательно посмотрим на код и поймем. Что справедливо до начала цикла, после каждой итерации и в конце? А справедливо следующее – если мы находимся на данной конкретной итерации, значит все предыдущие попытки найти значение провалились. Итак, инвариант выглядит следующим образом:

\(arr[i-1]eq T\), где arr — массив, i — текущее значение счетчика, T — искомое значение

Давайте теперь по порядку пройдемся и докажем справедливость подобного условия.

  • Инициализация. Значение справедливо, так как значение для индекса i — 1 не существует, а значит точно не равно T.
  • Сохранение. Если выполняется очередная итерация, значит позиция искомого значения всё еще не была найдена. Поэтому все значения для индекса j < i не будут равны T.
  • После выполнения цикла мы получим две ситуации. Либо мы нашли i, который указывает на найденный элемент, либо i = n. В любом случае, вне зависимости от того, нашли мы элемент или нет, все предыдущие элементы массива нам не подходили, а значит все значения для индекса j < i не равны T.

Зависит ли найденное условие от переменной, изменяющейся в теле цикла? Конечно, мы используем i, который, увеличиваясь на каждой итерации, поочередно указывает на каждый элемент массива до тех пор, пока значения не будет найдено, либо цикл не достигнет конца массива. Следовательно, данное условие можно с полной уверенностью считать инвариантом цикла.

Разумеется, далеко не все задачи решаются с помощью циклических алгоритмов. Например, наша реализация двоичного поиска из прошлой статьи была написана с помощью рекурсии.

Но как доказать корректность алгоритма в этом случае? Конечно, можно воспользоваться инвариантом и для рекурсивной функции, находя условие, которое будет совпадать до вызовов, в каждом вызове и после всех вложенных вызовов.

Но мы воспользуемся более общим методом доказательства – методом математической индукции.

Метод математической индукции

Допустим у нас есть некоторое утверждение P. Для того, чтобы доказать его истинность для всех натуральных чисел n нужно проделать несколько шагов:

  • Доказать, что P истинно в самом простом случае — для n = 1. Это называется базой индукции.
  • Далее мы предполагаем, что утверждение верно для некоторого k и доказываем, что если оно верно для k, то верно и для k + 1. Это называется шагом индукции или индукционным переходом.

Если мы это доказываем, тогда можем сделать вывод о том, что утверждение P справедливо для всех n.

Чисто математические примеры можете поискать сами, а я перейду непосредственно к алгоритмам.

Давайте для примера докажем корректность алгоритма двоичного поиска. На всякий случай приведу его код:

int binary_search(int arr[], int start, int end, int target) { if (start == end) { return arr[start] == target ? start : -1; } int mid = floor(start + (end — start) / 2); if (target

Нам нужно найти утверждение, которое будет зависеть от n. Для доказательства корректности работы нам достаточно показать, что алгоритм завершает работу за конечное число шагов.

Почему так? Если алгоритм завершается, то это означает, что функция, разбивая массив на две части и вызывая сама себя с нужным подмассивом, рано или поздно оказывается на самом нижнем уровне рекурсии, где имеет дело с массивом, содержащим один единственный элемент. Если это произошло, то алгоритму остается выполнить только операцию сравнения и вернуть значение.

Доказательство операции сравнения тривиально, поэтому нам нужно удостоверится только в том, что при любых предусмотренных входных данных алгоритм корректно завершится и значение будет возвращено. Поехали.

Для начала давайте подсчитаем количество рекурсивных вызовов. Я это уже сделал, поэтому просто скажу — \(\left\lceil \log _{ 2 }{ n } \right\rceil\). Поскольку при каждом вызове функции массив разбивается на две части, то увеличение n в 2 раза лишь добавляет один единственный шаг.

Мы округляем значение в большую сторону, так как mid всегда округляется (в меньшую сторону в данном случае), а значит при n, которое не кратно 2, у нас образуется двоякая ситуация, когда, в случае, если элемент расположен в правой части, алгоритм выполнит на 1 шаг больше.

Для описания мы и будем использовать этот «худший» случай.

В итоге доказательство сводится к тому, что нужно определить, что корректно выполняется самый нижний уровень рекурсии (когда вызывается функция с одним элементом), а после чего доказать, что самый нижний уровень действительно достижим.

  • \(\left\lceil \log _{ 2 }{ n } \right\rceil=0\). При вызове функции с массивом из одного элемента цепочка вызовов прекращается, так как алгоритм натыкается на оператор return, который возвращает позицию найденного элемента, либо -1.
  • Далее предполагаем, что наше утверждение верно для k = n.
  • Докажем, что результатом \(\left\lceil \log _{ 2 }{ k+1 } \right\rceil\) будет натуральное число — k является натуральным числом, а логарифм любого натурального числа не может быть отрицательным числом. Получившийся ответ округляется в большую сторону, что также делает его натуральным числом.

Следующая статья

Алгоритмы (теория/практика): Часть 6.1. «Разделяй и властвуй»

Предыдущая статья

Алгоритмы (теория/практика): Часть 4. Начинаем анализировать

Источник: https://blog.underpowered.net/algorithms/algoritmy-teoriya-praktika-chast-5-korrektnost-algoritmov/

Все термины
Добавить комментарий

;-) :| :x :twisted: :smile: :shock: :sad: :roll: :razz: :oops: :o :mrgreen: :lol: :idea: :grin: :evil: :cry: :cool: :arrow: :???: :?: :!: