В информатике, инвариант цикла является свойством программы цикла, что является истинным, прежде чем (и после) каждой итерации. Это логическое утверждение, которое иногда проверяется в коде с помощью вызова утверждения. Знание его инварианта (ов) важно для понимания эффекта цикла.
В формальной верификации программ, особенно в подходе Флойда-Хоара, инварианты циклов выражаются формальной логикой предикатов и используются для доказательства свойств циклов и алгоритмов расширения , которые используют циклы (обычно свойства корректности ). Инварианты цикла будут истинными при входе в цикл и после каждой итерации, так что при выходе из цикла могут быть гарантированы как инварианты цикла, так и условие завершения цикла.
С точки зрения методологии программирования, инвариант цикла можно рассматривать как более абстрактную спецификацию цикла, которая характеризует более глубокую цель цикла за пределами деталей этой реализации. Обзорная статья охватывает фундаментальные алгоритмы из многих областей информатики (поиск, сортировка, оптимизация, арифметика и т. Д.), Характеризуя каждый из них с точки зрения его инварианта.
Из-за сходства циклов и рекурсивных программ, доказательство частичной корректности циклов с инвариантами очень похоже на доказательство корректности рекурсивных программ с помощью индукции. Фактически, инвариант цикла часто совпадает с индуктивной гипотезой, которая должна быть доказана для рекурсивной программы, эквивалентной данному циклу.
Следующая подпрограмма C возвращает максимальное значение в своем массиве аргументов при условии, что его длина не менее 1. Комментарии предоставляются в строках 3, 6, 9, 11 и 13. Каждый комментарий содержит утверждение о значениях одной или нескольких переменных. на этом этапе функции. Выделенные утверждения в теле цикла в начале и в конце цикла (строки 6 и 11) абсолютно одинаковы. Таким образом, они описывают инвариантное свойство цикла. Когда достигается строка 13, этот инвариант все еще сохраняется, и известно, что условие цикла из строки 5 стало ложным. Оба свойства вместе означают, что оно равно максимальному значению в, то есть правильное значение возвращается из строки 14. max()
a[]
n
i!=n
m
a[0...n-1]
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 lt; 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 лучше изменить на ilt;n
, чтобы избежать бесконечного цикла для недопустимых отрицательных значений n
. Хотя это изменение в коде интуитивно не должно иметь никакого значения, рассуждения, ведущие к его правильности, становятся несколько более сложными, поскольку тогда igt;=n
известно только в строке 13. Чтобы получить это также ilt;=n
, это условие должно быть включено в цикл. инвариантный. Легко видеть, что это ilt;=n
также является инвариантом цикла, поскольку ilt;n
в строке 6 может быть получено из (модифицированного) условия цикла в строке 5 и, следовательно, ilt;=n
выполняется в строке 11 после i
увеличения в строке 10. Однако, когда инварианты цикла должны быть предоставлены вручную для формальной проверки программы, такие интуитивно слишком очевидные свойства, как ilt;=n
часто игнорируются.
В Флойда-Хоара логике, то частичная корректность из время цикла определяется по следующему правилу вывода:
Это означает:
Другими словами: приведенное выше правило является дедуктивным шагом, в основе которого лежит тройка Хоара. Эта тройка на самом деле является отношением состояний машины. Он сохраняется всякий раз, когда, начиная с состояния, в котором логическое выражение истинно, и при успешном выполнении некоторого вызванного кода, машина оказывается в состоянии, в котором I истинно. Если это отношение может быть доказано, то правило позволяет нам сделать вывод, что успешное выполнение программы приведет из состояния, в котором I истинно, к состоянию, в котором выполняется. Логическая формула I в этом правиле называется инвариантом цикла.
В следующем примере показано, как работает это правило. Рассмотрим программу
while (x lt; 10) x := x+1;
Тогда можно доказать следующую тройку Хоара:
Условие С из while
петли. Надо угадать полезный инвариант цикла I ; окажется, что это уместно. При этих предположениях можно доказать следующую тройку Хоара:
Хотя эта тройка формально может быть получена из правил логики Флойда-Хоара, регулирующих присваивание, она также интуитивно оправдана: вычисление начинается в состоянии, где истинно, что означает просто, что это правда. Вычисление прибавляет 1 к x, что означает, что это все еще верно (для целого числа x).
Исходя из этой предпосылки, правило while
петель позволяет сделать следующий вывод:
Однако постусловие ( x меньше или равно 10, но не меньше 10) логически эквивалентно тому, что мы хотели показать.
Свойство - это еще один инвариант цикла примера, а тривиальное свойство - еще одно. Применение приведенного выше правила вывода к предыдущим инвариантным доходам. Применяя его к инвариантной доходности, что немного более выразительно.
Язык программирования Eiffel обеспечивает встроенную поддержку инвариантов цикла. Инвариант цикла выражается тем же синтаксисом, что и инвариант класса. В приведенном ниже примере выражение инварианта цикла x lt;= 10
должно быть истинным после инициализации цикла и после каждого выполнения тела цикла; это проверяется во время выполнения.
from x:= 0 invariant x lt;= 10 until x gt; 10 loop x:= x + 1 end
Язык программирования Whiley также обеспечивает первоклассную поддержку инвариантов цикла. Инварианты цикла выражаются с помощью одного или нескольких where
предложений, как показано ниже:
function max(int[] items) -gt; (int r) // Requires at least one element to compute max requires |items| gt; 0 // (1) Result is not smaller than any element ensures all { i in 0..|items| | items[i] lt;= 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 lt; |items| // (1) No item seen so far is larger than m where all { k in 0..i | items[k] lt;= m } // (2) One or more items seen so far matches m where some { k in 0..i | items[k] == m }: if items[i] gt; m: m = items[i] i = i + 1 // return 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. существуют некоторые инструменты для поддержки математических доказательств, обычно основанные на показанном выше правиле Флойда – Хоара, что данный код цикла фактически удовлетворяет заданному (набору) инварианту (ам) цикла.
Технику абстрактной интерпретации можно использовать для автоматического определения инварианта цикла данного кода. Однако этот подход ограничен очень простыми инвариантами (такими как 0lt;=i amp;amp; ilt;=n amp;amp; i%2==0
).
Инвариант цикла ( свойство инвариантности цикла) следует отличать от кода, инвариантного к циклу ; обратите внимание на «инвариант цикла» (существительное) и «инвариант цикла» (прилагательное). Код, инвариантный к циклам, состоит из операторов или выражений, которые можно переместить за пределы тела цикла, не влияя на семантику программы. Такие преобразования, называемые движением кода с инвариантным циклом, выполняются некоторыми компиляторами для оптимизации программ. Пример кода, инвариантного к циклам (на языке программирования C ):
for (int i=0; ilt;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; ilt;n; ++i) { a[i] = 6*i + t1; }
Напротив, например, свойство 0lt;=i amp;amp; ilt;=n
является инвариантом цикла как для исходной, так и для оптимизированной программы, но не является частью кода, поэтому не имеет смысла говорить о «перемещении его из цикла».
Код, инвариантный к циклам, может вызывать соответствующее свойство, инвариантное к циклам. Для приведенного выше примера самый простой способ увидеть это - рассмотреть программу, в которой инвариантный код цикла вычисляется как до, так и внутри цикла:
x1 = y+z; t1 = x1*x1; for (int i=0; ilt;n; ++i) { x2 = y+z; a[i] = 6*i + t1; }
Свойство этого кода (x1==x2 amp;amp; t1==x2*x2) || i==0
, инвариантное к циклу, указывает, что значения, вычисленные перед циклом, согласуются со значениями, вычисленными внутри (за исключением перед первой итерацией).