Каков наилучший способ определения инварианта цикла?

Question

При использовании формальных аспектов для создания некоторого кода существует ли общий метод определения инварианта цикла или он будет полностью отличаться в зависимости от проблемы?

Answer 1

Уже указывалось, что один и тот же цикл может иметь несколько инвариантов, и что вычислимость против вас. Это не значит, что вы не можете попробовать.

На самом деле вы ищете индуктивный инвариант : слово-инвариант может также использоваться для свойства, которое истинно на каждой итерации, но для которого недостаточно знать, что оно выполняется в одна итерация, чтобы вывести, что она имеет место на следующей. Если I является индуктивным инвариантом, то любое последствие I является инвариантом, но не может быть индуктивным инвариантом.

Вы, вероятно, пытаетесь получить индуктивный инвариант для доказательства определенного свойства (постусловия) цикла в некоторых определенных обстоятельствах (предварительных условиях).

Есть две эвристики, которые работают довольно хорошо:

• начните с того, что у вас есть (предварительные условия), и ослабляйте, пока у вас не будет индуктивного инварианта. Чтобы понять, как ослабить, примените одну или несколько итераций прямого цикла и посмотрите, что перестает быть верным в вашей формуле.

• начните с того, что вы хотите (постусловия) и укрепляйте, пока у вас не будет индуктивного инварианта. Чтобы понять, как укрепить, примените одну или несколько итераций цикла в обратном направлении и посмотрите, что нужно добавить, чтобы можно было вывести постусловие.

Если вы хотите, чтобы компьютер помог вам в вашей практике, я могу порекомендовать плагин дедуктивной верификации Jessie для C-программ Frama-C . Есть и другие, особенно для аннотаций Java и JML, но я менее знаком с ними. Испытывать инварианты, о которых вы думаете, гораздо быстрее, чем работать, если они работают на бумаге. Я должен отметить, что проверка того, что свойство является индуктивным инвариантом, также неразрешима, но современные автоматические средства проверки хороши на многих простых примерах. Если вы решите пойти по этому пути, возьмите из списка как можно больше: Alt-ergo, Simplify, Z3.

С опциональной (и немного сложной для установки) библиотекой Apron Джесси также может автоматически выводить некоторые простые инварианты .

Answer 2

На самом деле тривиально генерировать циклические инварианты. true хороший пример. Он выполняет все три свойства, которые вы хотите:

1. Держится до входа в цикл
2. Держится после каждой итерации
3. Держится после завершения цикла

Но то, что вы ищете, это, вероятно, самый сильный * инвариант цикла . Однако нахождение самого сильного инварианта цикла иногда является задачей неразрешимой . См. Статью Неадекватность вычислимых инвариантов цикла .

Answer 3

Я не думаю, что это легко автоматизировать. Из вики:

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

Answer 4

Я написал о написании инвариантов цикла в своем блоге, см. Проверка циклов, часть 2 . Инварианты, необходимые для доказательства правильности цикла, обычно состоят из 2 частей:

1. Обобщение состояния, которое предполагается, когда цикл завершается.
2. Дополнительные биты, необходимые для обеспечения правильного формирования тела цикла (например, индексы массива в границах).

(2) прост. Чтобы получить (1), начните с предиката, выражающего желаемое состояние после завершения. Скорее всего, он содержит «данные» или «существует» в некотором диапазоне данных. Теперь измените границы «forall» или «существует» так, чтобы (а) они зависели от переменных, измененных циклом (например, счетчики цикла), и (б) так, чтобы инвариант был тривиально истинным при первом входе в цикл обычно пустым диапазоном «forall» или «существует»).

Answer 5

Существует несколько эвристик для нахождения инвариантов цикла. Одна хорошая книга об этом - «Программирование в 1990-х» Эд Коэн. Речь идет о том, как найти хороший инвариант, манипулируя постусловием вручную. Примеры: заменить константу на переменную, усилить инвариант, ...