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

Инварианты, используемые для доказательства свойств циклов

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

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

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

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

Неофициальный пример

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

int max ( int n , const int a []) {       интервал м = а [ 0 ];    // m равно максимальному значению в a[0...0] интервал я = 1 ;    в то время как ( я != п ) {     // m равно максимальному значению в a[0...i-1] если ( м < а [ я ])    м = а [ я ];   // m равно максимальному значению в a[0...i] ++ я ; // m равно максимальному значению в a[0...i-1] } // m равно максимальному значению в a[0...i-1], и i==n вернуть м ; }

Следуя парадигме защитного программирования , условие цикла 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 определяется следующим правилом вывода:

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

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

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

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

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

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

P & c { seq } P

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

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

Пример

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

в то время как (х < 10) х := х+1;

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

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

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

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

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

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

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

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

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

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

Эйфелева

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

 от x := 0 инвариант x <= 10 до x > 10 цикл x := x + 1 конец                  

Пока

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

function  max ( int ​​[]  items )  ->  ( int  r ) // Для вычисления max требуется хотя бы один элемент | предметы | > 0 // (1) Результат не меньше любого элемента, гарантирует, что все { i in 0 .. | предметы | | items [ i ] <= r } // (2) Результат соответствует хотя бы одному элементу, что гарантирует некоторое { i in 0 .. | предметы | | items [ i ] == r } : // nat i = 1 int m = items [ 0 ] // while i < | предметы | // (1) Ни один из наблюдаемых на данный момент элементов не превышает m, где все { k in 0 .. i | items [ k ] <= m } // (2) Один или несколько элементов, замеченных на данный момент, соответствуют m , где some { k in 0 .. i | items [ k ] == m } : if items [ i ] > m : m = items [ i ] i = i + 1 // возвращаем m                                                                            

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

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

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

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

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

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

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

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

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

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

для ( int я знак равно 0 ; я < п ; ++ я ) { Икс знак равно y + z ; а [ я ] знак равно 6 * я + х * х ; }             

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

Икс знак равно у + z ; т1 = х * х ; для ( int я знак равно 0 ; я < п ; ++ я ) { а [ я ] знак равно 6 * я + t1 ; }              

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

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

х1 = у + z ; т1 = х1 * х1 ; для ( int я знак равно 0 ; я < п ; ++ я ) { x2 знак равно y + z ; а [ я ] знак равно 6 * я + т1 ; }                 

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

Смотрите также

• Инвариант (информатика)
• Движение кода, инвариантное к циклу
• Петлевой вариант
• Слабейшие предварительные условия цикла while

Рекомендации

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 г.
4. Конвей, Ричард ; Грис, Дэвид (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. doi : 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 года.
• Майкл Хут, Марк Райан. «Логика в информатике», второе издание.