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

Ответ 1

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

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

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

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

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

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

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

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

Ответ 2

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

• Он сохраняется до записи цикла
• Он сохраняется после каждой итерации
• Он поддерживает завершение цикла

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

Ответ 3

Мне нелегко автоматизировать это. Из wiki:

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

Ответ 4

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

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

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

Ответ 5

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