🖥️ Математика, Информатика и Инженерия ПО

11. Инвариант цикла (на примере задачи сортировки)

время чтения ~6 мин.

ВПЕРЁД ⇒

Сортировка вставками (insertion sort)

⇐ НАЗАД

Асимптотическое обозначение тета-большое


Инвариант цикла (на примере задачи сортировки)

Постановка задачи сортировки

Задача:

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

Ключевым словом в поставленной задаче является слово порядок. С математической точки зрения элементы массива находятся в отношении порядка, то есть могут быть сравнены между собой. Поскольку элементы массива могут быть сравнены между собой, то из этого следует, что они также могут быть переупорядочены (то есть могут быть отсортированы).

Алгоритм сортировки в простом случае предполагает выполнение некоторых повторяющихся/циклических действий по перестановке элементов массива до тех пор, пока все его элементы не окажутся отсортированными. Эти повторяющиеся/циклические действия именуются итерациями цикла (проходами тела цикла). Таким образом, рассматриваемый нами алгоритм сортировки будет содержать итерации цикла.

Понятие инварианта цикла

Когда алгоритм можно декомпозировать (разбить) на итерации, то для проверки корректности работы всего алгоритма поступают следующим образом:

  • Очевидно, что правильность работы всего алгоритма зависит от правильности выполнения итераций. Если мы хотим определить, корректно ли выполняются итерации, нам необходимо выбрать некоторое свойство цикла, которое будет являться неизменным от итерации к итерации. Такое свойство в программировании носит название инварианта цикла. Мы выбираем инвариант цикла, исходя из целей задачи.
  • Когда инвариант цикла выбран, мы проверяем, что этот инвариант остаётся неизменным на протяжении работы всего алгоритма.
  • Количество итераций цикла обязано быть конечным, то есть алгоритм обязан рано или поздно завершить свою работу и возвратить результат этой работы. Если алгоритм выполняется бесконечно долго (то есть зависает на этапе исполнения) и не возвращает никакого результата, то нет никакой пользы от использования подобного алгоритма в какой бы то ни было программе.

Примечание

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

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

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

Доказательство корректности любого произвольного цикла с применением инварианта

Порядок доказательства корректности любого произвольного цикла с помощью инварианта сводится к следующему:

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

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

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

    Примечание

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

    Таким образом, хоть принцип математической индукции и является полезным в получении доказательства соблюдения инварианта среди всех элементов последовательности, однако, используя данный принцип, нельзя сделать вывод о том, является ли рассматриваемая последовательность конечной. Иными словами, используя только лишь один принцип математической индукции, нельзя доказать, что цикл завершается (состоит из конечного числа итераций), что означает существование необходимости как-то отдельно доказывать завершаемость цикла.

  2. Доказывается, что цикл завершится, то есть условие завершения рано или поздно будет выполнено.

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

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

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

  1. Инициализация. Инварианты справедливы перед первой итерацией цикла.
  2. Сохранение. Если инварианты справедливы перед очередной итерацией цикла, то эти инварианты справедливы и по окончании данной итерации.
  3. Завершение. По завершении цикла инварианты позволяют убедиться в правильности алгоритма.

Мы можем подытожить вышесказанное следующим образом:

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

Корректность и инвариант цикла в задачах сортировки

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

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

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


ВПЕРЁД ⇒

Сортировка вставками (insertion sort)

⇐ НАЗАД

Асимптотическое обозначение тета-большое


Вид графа

Обратные ссылки