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

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

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

С точки зрения методологии программирования инвариант цикла можно рассматривать как более абстрактную спецификацию цикла, которая характеризует более глубокое назначение цикла, выходящее за рамки деталей этой реализации. Обзорная статья ^[1] охватывает фундаментальные алгоритмы из многих областей информатики (поиск, сортировка, оптимизация, арифметика и т. д.), характеризуя каждый из них с точки зрения его инварианта.

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

Неофициальный пример [ править ]

Следующая C подпрограмма max() возвращает максимальное значение в своем массиве аргументов a[], при условии его длины n это как минимум 1. Комментарии предоставляются в строках 3, 6, 9, 11 и 13. Каждый комментарий утверждает о значениях одной или нескольких переменных на этом этапе функции. Выделенные утверждения внутри тела цикла в начале и конце цикла (строки 6 и 11) абсолютно одинаковы. Таким образом, они описывают инвариантное свойство цикла. Когда достигается строка 13, этот инвариант все еще сохраняется, и известно, что условие цикла i!=n из строки 5 стало ложным. Оба свойства вместе подразумевают, что m равно максимальному значению в a[0...n-1], то есть из строки 14 возвращается правильное значение.

int max(int n, const int a[]) {
    int m = a[0];
    // m equals the maximum value in a[0...0]
    int i = 1;
    while (i != n) {
        // m equals the maximum value in a[0...i-1]
        if (m < a[i])
            m = a[i];
        // m equals the maximum value in a[0...i]
        ++i;
        // m equals the maximum value in a[0...i-1]
    }
    // m equals the maximum value in a[0...i-1], and i==n
    return m;
}

Следуя парадигме защитного программирования , условие цикла i!=n в строке 5 лучше изменить на i<n, чтобы избежать бесконечного цикла для недопустимых отрицательных значений n. Хотя интуитивно это изменение в коде не должно иметь никакого значения, рассуждения, ведущие к его правильности, становятся несколько сложнее, поскольку только тогда i>=n известно в строке 13. Чтобы получить это также i<=n выполняется, это условие должно быть включено в инвариант цикла. Это легко увидеть i<=nтакже является инвариантом цикла, поскольку i<n в строке 6 может быть получено из (модифицированного) условия цикла в строке 5, и, следовательно, i<=n хранится в строке 11 после i было увеличено в строке 10. Однако, когда инварианты цикла приходится вручную указывать для формальной проверки программы, такие интуитивно слишком очевидные свойства, как i<=n часто упускаются из виду.

Логика Флойда-Хора [ править ]

В -Хора логике Флойда ^[2]^[3] Частичная корректность цикла while определяется следующим правилом вывода:

{\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;{\mathtt {while}}\ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}

Это означает:

Если какое-то свойство $I$ сохраняется кодом $\mathrm {body}$ — точнее, если $I$ удерживается после выполнения $\mathrm {body}$ всякий раз, когда и $C$ , и $я$ держали заранее — (верхняя строка), тогда
$C$ и $I$ гарантированно будут ложными и истинными соответственно после выполнения всего цикла ${\mathtt {while}}\ (C)\ \mathrm {body}$ , при условии, что $я$ перед циклом был прав (нижняя строка) .

Другими словами: приведенное выше правило представляет собой дедуктивный шаг, в основе которого лежит тройка Хоара. $\{C\land I\}\;\mathrm {body} \;\{I\}$ . Эта тройка на самом деле является отношением состояний машины. Он сохраняется всякий раз, когда начинается с состояния, в котором логическое выражение $C\land I$ верно и успешно выполняет некоторый код под названием $\mathrm {body}$ , машина попадает в состояние, в котором $я$ прав. Если это соотношение может быть доказано, правило позволяет нам заключить, что успешное выполнение программы ${\mathtt {while}}\ (C)\ \mathrm {body}$ приведет из состояния, в котором $я$ верен, в состояние, в котором $\lnot C\land I$ держит. Булева формула $I$ в этом правиле называется инвариантом цикла.

С некоторыми изменениями в используемых обозначениях и предпосылкой остановки цикла это правило также известно как теорема об инвариантных отношениях . ^[4]^[5] В одном из учебников 1970-х годов это представлено так, чтобы оно было доступно студентам-программистам: ^[4]

Пусть обозначения P { seq } Q имею в виду, что если P истинно перед последовательностью утверждений seq беги, тогда Q правда после этого. Тогда справедлива теорема об инвариантном соотношении, что

P & c { seq } P

подразумевает

P { DO WHILE (c); seq END; } P & ¬c

Пример [ править ]

Следующий пример иллюстрирует, как работает это правило. Рассмотрим программу

while (x < 10)
    x := x+1;

Тогда можно доказать следующую тройку Хоара:

\{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{x=10\}

Условие С while цикл это $x<10$ . Полезный инвариант цикла, $как я$ должен догадаться; окажется, что $x\leq 10$ подходит. При этих предположениях можно доказать следующую тройку Хоара:

\{x<10\land x\leq 10\}\;x:=x+1\;\{x\leq 10\}

Хотя эта тройка может быть формально выведена из правил логики Флойда-Хора, управляющей присваиванием, она также интуитивно оправдана: вычисление начинается в состоянии, когда $x<10\land x\leq 10$ это правда, что означает просто, что $x<10$ это правда. Вычисление добавляет 1 к $x$ , что означает, что $x\leq 10$ по-прежнему верно (для целого числа x).

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

\{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{\lnot (x<10)\land x\leq 10\}

Однако постусловие $\lnot (x<10)\land x\leq 10$ ( $x$ меньше или равно 10, но не меньше 10) логически эквивалентно $x=10$ , это то, что мы хотели показать.

Недвижимость $0\leq x$ — еще один инвариант цикла примера, а тривиальное свойство $\mathrm {true}$ это еще один. Применение приведенного выше правила вывода к прежним инвариантам дает $\{0\leq x\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ . Применяя его к инварианту $\mathrm {true}$ урожайность $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$ , что несколько более выразительно.

Поддержка языков программирования [ править ]

Эйфелева [ править ]

Язык программирования Eiffel обеспечивает встроенную поддержку инвариантов цикла. ^[6] Инвариант цикла выражается с помощью того же синтаксиса, который используется для инварианта класса . В примере ниже выражение, инвариантное к циклу x <= 10 должно быть истинным после инициализации цикла и после каждого выполнения тела цикла; это проверяется во время выполнения.

    from
        x := 0
    invariant
        x <= 10
    until
        x > 10
    loop
        x := x + 1
    end

Пока [ править ]

Язык программирования Whiley также обеспечивает первоклассную поддержку инвариантов циклов. ^[7] Инварианты цикла выражаются с использованием одного или нескольких where пунктов, как показано ниже:

function max(int[] items) -> (int r)
// Requires at least one element to compute max
requires |items| > 0
// (1) Result is not smaller than any element
ensures all { i in 0..|items| | items[i] <= r }
// (2) Result matches at least one element
ensures some { i in 0..|items| | items[i] == r }:
    //
    nat i = 1
    int m = items[0]
    //
    while i < |items|
    // (1) No item seen so far is larger than m
    where all { k in 0..i | items[k] <= m }
    // (2) One or more items seen so far matches m
    where some { k in 0..i | items[k] == m }:
        if items[i] > m:
            m = items[i]
        i = i + 1
    //
    return m

The max() Функция определяет наибольший элемент целочисленного массива. Чтобы это было определено, массив должен содержать хотя бы один элемент. Постусловия max() требовать, чтобы возвращаемое значение было: (1) не меньше любого элемента; и (2) что он соответствует хотя бы одному элементу. Инвариант цикла определяется индуктивно через два where предложения, каждое из которых соответствует предложению постусловия. Фундаментальное отличие состоит в том, что каждое предложение инварианта цикла идентифицирует результат как правильный до текущего элемента. i, а постусловия идентифицируют результат как правильный для всех элементов.

Использование инвариантов цикла [ править ]

Инвариант цикла может служить одной из следующих целей:

чисто документальный
проверяться внутри кода, например, с помощью вызова утверждения
подлежит проверке на основе подхода Флойда-Хора

Для 1. комментарий на естественном языке (например, // m equals the maximum value in a[0...i-1] в приведенном выше примере) достаточно.

Для версии 2. требуется поддержка языков программирования, таких как C библиотека Assert.h или выше . показанная invariant пункт в Эйфеле. Часто проверку во время выполнения можно включать (для отладочных запусков) и отключать (для рабочих запусков) с помощью компилятора или опции времени выполнения. ^{[ нужна ссылка ]}

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

Технику абстрактной интерпретации можно использовать для автоматического обнаружения инварианта цикла данного кода. Однако этот подход ограничен очень простыми инвариантами (такими как 0<=i && i<=n && i%2==0).

Отличие от кода, инвариантного к циклу [ править ]

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

for (int i=0; i<n; ++i) {
    x = y+z;
    a[i] = 6*i + x*x;
}

где расчеты x = y+z и x*x можно переместить перед циклом, в результате чего получится эквивалентная, но более быстрая программа:

x = y+z;
t1 = x*x;
for (int i=0; i<n; ++i) {
    a[i] = 6*i + t1;
}

Напротив, например, свойство 0<=i && i<=n является инвариантом цикла как для исходной, так и для оптимизированной программы, но не является частью кода, поэтому не имеет смысла говорить о «выведении его из цикла».

Код, инвариантный к циклу, может вызывать соответствующее свойство инвариантности к циклу. ^{[ нужны разъяснения ]} В приведенном выше примере самый простой способ увидеть это — рассмотреть программу, в которой код инварианта цикла вычисляется как до, так и внутри цикла:

x1 = y+z;
t1 = x1*x1;
for (int i=0; i<n; ++i) {
    x2 = y+z;
    a[i] = 6*i + t1;
}

Свойство этого кода, инвариантное к циклу, (x1==x2 && t1==x2*x2) || i==0, указывая, что значения, вычисленные перед циклом, совпадают со значениями, вычисленными внутри него (кроме случаев до первой итерации).

См. также [ править ]

Ссылки [ править ]

^ Карло А. Фуриа, Бертран Мейер и Сергей Вельдер. «Инварианты циклов: анализ, классификация и примеры». Обзоры вычислений ACM. том. 46, нет. 3 февраля 2014 г.( [1]
^ Роберт В. Флойд (1967). «Придание значения программам» (PDF) . В Дж. Т. Шварце (ред.). Материалы симпозиумов по прикладной математике . Математические аспекты информатики. Том. 19. Провиденс, Род-Айленд: Американское математическое общество. стр. 19–32.
^ Хоар, ЦАР (октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID 207726175 . Архивировано из оригинала (PDF) 4 марта 2016 г.
^ Jump up to: Перейти обратно: ^а ^б Конвей, Ричард ; Грис, Дэвид (1973). Введение в программирование: структурированный подход с использованием PL/1 и PL/C . Кембридж, Массачусетс: Уинтроп. стр. 198–200.
^ Хуанг, JC (2009). Обнаружение ошибок программного обеспечения посредством тестирования и анализа . Хобокен, Нью-Джерси: John Wiley & Sons. стр. 156–157.
^ Мейер, Бертран , Эйфель: Язык, Prentice Hall , 1991, стр. 129–131.
^ Пирс, Дэвид Дж.; Гроувс, Линдси (2015). «Проектирование проверяющего компилятора: уроки, извлеченные из разработки Whiley». Наука компьютерного программирования . 113 : 191–220. дои : 10.1016/j.scico.2015.09.006 .

Дальнейшее чтение [ править ]

Томас Х. Кормен , Чарльз Э. Лейзерсон , Рональд Л. Ривест и Клиффорд Стейн . Введение в алгоритмы , второе издание. MIT Press и McGraw-Hill, 2001. ISBN 0-262-03293-7 . Страницы 17–19, раздел 2.1: Сортировка вставками.
Дэвид Грайс . « Заметка о стандартной стратегии разработки инвариантов и циклов цикла ». Наука компьютерного программирования , том 2, стр. 207–214. 1984.
Майкл Д. Эрнст, Джейк Кокрелл, Уильям Грисволд, Дэвид Ноткин. « Динамическое обнаружение вероятных инвариантов программы для поддержки эволюции программы ». Международная конференция по программной инженерии , стр. 213–224. 1999.
Роберт Пейдж. « Программирование с инвариантами ». Программное обеспечение IEEE , 3(1):56–69. Январь 1986 года.
Яньхун А. Лю, Скотт Д. Столлер и Тим Тейтельбаум . Усиление инвариантов для эффективных вычислений . Наука компьютерного программирования , 41(2):139–172. Октябрь 2001 года.
Майкл Хут, Марк Райан. « Логика в информатике », второе издание.

[1] Карло А. Фуриа, Бертран Мейер и Сергей Вельдер. «Инварианты циклов: анализ, классификация и примеры». Обзоры вычислений ACM. том. 46, нет. 3 февраля 2014 г.( [1]

[2] Роберт В. Флойд (1967). «Придание значения программам» (PDF) . В Дж. Т. Шварце (ред.). Материалы симпозиумов по прикладной математике . Математические аспекты информатики. Том. 19. Провиденс, Род-Айленд: Американское математическое общество. стр. 19–32.

[3] Хоар, ЦАР (октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID 207726175 . Архивировано из оригинала (PDF) 4 марта 2016 г.

[conway-gries-4] Jump up to: Перейти обратно: ^а ^б Конвей, Ричард ; Грис, Дэвид (1973). Введение в программирование: структурированный подход с использованием PL/1 и PL/C . Кембридж, Массачусетс: Уинтроп. стр. 198–200.

[5] Хуанг, JC (2009). Обнаружение ошибок программного обеспечения посредством тестирования и анализа . Хобокен, Нью-Джерси: John Wiley & Sons. стр. 156–157.

[6] Мейер, Бертран , Эйфель: Язык, Prentice Hall , 1991, стр. 129–131.

[7] Пирс, Дэвид Дж.; Гроувс, Линдси (2015). «Проектирование проверяющего компилятора: уроки, извлеченные из разработки Whiley». Наука компьютерного программирования . 113 : 191–220. дои : 10.1016/j.scico.2015.09.006 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]