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

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

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

С точки зрения методологии программирования, инвариант цикла можно рассматривать как более абстрактную спецификацию цикла, которая характеризует более глубокую цель цикла за пределами деталей этой реализации. Обзорная статья ^[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 [])  { int  m  =  a [ 0 ]; // m равно максимальному значению в [0 ... 0] int  я  =  1 ; while  ( i  ! =  n )  { // m равно максимальному значению в [0 ... i-1] если  ( m  <  a [ i ]) т  =  а [ я ]; // m равно максимальному значению в [0 ... i] ++ i ; // m равно максимальному значению в [0 ... i-1] } // m равно максимальному значению в [0 ... i-1], а 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] частичная корректность из время цикла регулируется с помощью следующего правила вывода:

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

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

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

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

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

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

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

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

{\ Displaystyle \ {х \ Leq 10 \} \; \ mathbf {while} \ (х <10) \ х: = х + 1 \; \ {х = 10 \}}

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

{\ Displaystyle \ {х <10 \ земля х \ leq 10 \} \; х: = х + 1 \; \ {х \ leq 10 \}}

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

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

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

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

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

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

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

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

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

В то время как [ править ]

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

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

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

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

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

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

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

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

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

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

Отличие от неизменяемого цикла кода [ править ]

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

для  ( int  i = 0 ;  i < n ;  ++ i )  {  x  =  y + z ;  а [ я ]  =  6 * я  +  х * х ; }

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

х  =  у + г ; t1  =  х * х ; для  ( int  i = 0 ;  i < n ;  ++ i )  {  a [ i ]  =  6 * i  +  t1 ; }

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

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

х1  =  у + г ; t1  =  x1 * x1 ; для  ( int  i = 0 ;  i < n ;  ++ i )  {  x2  =  y + z ;  а [ я ]  =  6 * я  +  t1 ; }

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

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

Инвариант (информатика)
Циклически-инвариантное движение кода
Вариант петли
Самые слабые предварительные условия цикла While

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

↑ Карло А. Фурия, [Бертран Мейер] и Сергей Велдер. «Инварианты цикла: анализ, классификация и примеры». ACM Computing Surveys. т. 46, нет. 3 февраля 2014 г. ( [1]
^ Роберт В. Флойд (1967). «Придание смысла программам» (PDF) . В JT Schwartz (ред.). Материалы симпозиумов по прикладной математике . Математические аспекты информатики. 19 . Провиденс, Род-Айленд: Американское математическое общество. С. 19–32.
Перейти ↑ Hoare, CAR (октябрь 1969). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации ACM . 12 (10): 576–580. DOI : 10.1145 / 363235.363259 . Архивировано из оригинального (PDF) 04 марта 2016 года.
Перейти ↑ Meyer, Bertrand , Eiffel: The Language, Prentice Hall , 1991, pp. 129–131.
^ Пирс, Дэвид Дж .; Гроувс, Линдси (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 г.
Майкл Хут, Марк Райан. « Логика в информатике », второе издание.

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

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

[3] Перейти ↑ Hoare, CAR (октябрь 1969). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации ACM . 12 (10): 576–580. DOI : 10.1145 / 363235.363259 . Архивировано из оригинального (PDF) 04 марта 2016 года.

[4] Перейти ↑ Meyer, Bertrand , Eiffel: The Language, Prentice Hall , 1991, pp. 129–131.

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

[1]