Инварианты петли могут дать вам сверхспособности кодирования

Инвариант - это утверждение о программных переменных, которое истинно каждый раз, когда выполнение программы достигает инварианта.

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

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

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

Определение инварианта петли

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

Хороший инвариант цикла должен удовлетворять трем свойствам:

1. Инициализация: инвариант цикла должен быть истинным перед первым выполнением цикла.
2. Обслуживание: если инвариант равен true перед итерацией цикла, он должен быть равен true и после итерации.
3. Завершение : Когда цикл завершается, инвариант должен сказать нам что-то полезное, что поможет нам понять алгоритм.

Давайте начнем с простого куска кода.

Algorithm sum(n) Input: a non-negative integer n Output: the sum 1 + 2 + … + n sum ← 0 i ← 1 while i ≤ n // Invariant: sum = 1 + 2 + … + (i - 1) sum ← sum + i i ← i + 1 return sum

В этом примере:

1. Инвариант цикла выполняется изначально, так как sum = 0и i = 1в этой точке. (Пустая сумма равна нулю.)
2. Предполагая, что инвариант выполняется до iитерации, он будет верен и после этой итерации, поскольку цикл добавляет iк сумме и увеличивает iна единицу.
3. Когда цикл вот-вот завершится, инвариант утверждает, что sum = 1 + 2 + … + nименно то, что нужно для правильности алгоритма.

Фактически, три вышеприведенных шага представляют собой доказательство индукции, которое показывает, что sum = 1 + 2 + … + nкогда программа выходит из цикла.

Проектирование с инвариантами

Мы можем использовать инвариант цикла при разработке алгоритма. Давайте начнем с этого скелета кода.

Algorithm max(A) Input: an array A storing n integers Output: the largest element in A max ← … for i = 0 to n-1 // Invariant: max = max(A[0], A[1], …, A[i-1]) … return max

Инвариант, кажется, выбран правильно: он удовлетворяет свойству завершения, так как переменная, max = max(A[0], A[1], …, A[n-1]) когда цикл завершается.

Мы можем попытаться удовлетворить свойство инициализации , присвоив подходящее начальное значение max. Однако не ясно, как определить максимальное значение пустого среза. Мы нашли потенциальную ошибку еще до написания любого кода! Одним из решений является изменение контракта функции.

Algorithm max(A) Input: an array A storing n integers, where n ≥ 1 Output: the largest element in A max ← … for i = 0 to n-1 // Invariant: max = max(A[0], A[1], …, A[i-1]) … return max

Теперь легко решить проблему. Если мы позволим max = A[0]и начнем цикл с i = 1, инвариант будет иметь место, когда мы впервые войдем в цикл.

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

Algorithm max(A) Input: an array A storing n integers, where n ≥ 1 Output: the largest element in A max ← A[0] for i = 1 to n-1 // Invariant: max = max(A[0], A[1], …, A[i-1]) if A[i] > max max ← A[i] return max

Сортировка

Algorithm sort(A) Input: an array A storing n integers Output: the same array with the elements sorted in ascending order for j = 1 to n-1 // Invariant: A[0..j-1] contains the same elements as // the original subarray A[0..j-1], but in sorted order. key ← A[j] i ← j - 1 while i ≥ 0 and A[i] > key A[i+1] ← A[i] i ← i - 1 A[i+1] ← key

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

Давайте посмотрим на свойство инициализации. Можно предположить, что срез содержит как минимум два элемента, поскольку цикл не будет выполняться в противном случае. (Это также не требуется, поскольку срез с не более чем одним элементом уже отсортирован.) Перед выполнением цикла инвариантные состояния « A[0..0]содержат те же элементы, что и исходный подмассив A[0..0], но в отсортированном порядке». Это явно верно.

Чтобы проверить свойство обслуживания, нам нужно внимательнее взглянуть на код. Можно предположить, что инвариант выполняется до цикла, т.е. A[0..j-1]отсортирован, и нужно только проверить, что код вставляет элемент A[j]в правильную позицию. Это достигается путем перемещения всех элементов A[j-1], A[j-2],…больше, чем на A[j] один шаг вправо, а затем вставки A[j]в правильное положение.

3-сторонняя перегородка

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