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

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

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

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

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

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

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

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

1. Инициализация: инвариант должен быть истинным перед первым выполнением цикла.
2. Сохранение: если инвариант истинен перед очередной итерацией, он должен оставаться истинным и после её завершения.
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 — инвариант выполняется с самого начала.

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

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

Завершение: когда внешний цикл заканчивается, инвариант говорит, что весь массив отсортирован. ✓

Инициализация: перед первой итерацией инвариант утверждает, что «A[0..0] содержит те же элементы, что исходный подмассив A[0..0], в отсортированном порядке» — что очевидно верно. ✓

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

Трёхстороннее разбиение

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

// Partition reorders the elements of v so that:
// - all elements in v[:low] are less than p,
// - all elements in v[low:high] are equal to p,
// - all elements in v[high:] are greater than p.
func Partition(v []int, p int) (low, high int) {
    low, high = 0, len(v)
    for mid := 0; mid < high; {
        // Invariant:
        //  - v[:low] < p
        //  - v[low:mid] = p
        //  - v[mid:high] are unknown
        //  - v[high:] > p
        //
        //         < p       = p        unknown       > p
        //     -----------------------------------------------
        // v: |          |          |a            |           |
        //     -----------------------------------------------
        //                ^          ^             ^
        //               low        mid           high
        switch a := v[mid]; {
        case a < p:
            v[mid] = v[low]
            v[low] = a
            low++
            mid++
        case a == p:
            mid++
        default: // a > p
            v[mid] = v[high-1]
            v[high-1] = a
            high--
        }
    }
    return
}

Дополнительные материалы

• Loop invariants: analysis, classification, and examples — ACM Computing Surveys 46, 3, Article 34 (январь 2014)
• Introduction: Developing and understanding loops — cs.cornell.edu
• On induction and recursive functions, with an application to binary search — yourbasic.org

Оригинал статьи: Loop invariants can give you coding superpowers — Stefan Nilsson, yourbasic.org. Лицензия CC BY 3.0.