Что лучший способ определить инвариант цикла?
Чтобы использование формальных аспектов создало некоторый код, там общий метод определения инварианта цикла, или это будет полностью отличаться в зависимости от проблемы?
4 ответа
Уже указывалось, что один и тот же цикл может иметь несколько инвариантов, и что вычислимость против вас. Это не значит, что нельзя пытаться.
Фактически вы ищете индуктивный инвариант : слово инвариант также может использоваться для свойства, которое истинно на каждой итерации, но для которого недостаточно знать, что оно выполняется на одна итерация, чтобы вывести, что она выполняется на следующей. Если I является индуктивным инвариантом, то любое следствие I является инвариантом, но может не быть индуктивным инвариантом.
Вы, вероятно, пытаетесь получить индуктивный инвариант для доказательства определенного свойства (постусловия) цикла в некоторых определенных обстоятельствах (предварительных условиях).
Есть две эвристики, которые работают достаточно хорошо:
начните с того, что у вас есть (предварительные условия), и ослабляйте, пока не получите индуктивный инвариант. Чтобы получить интуитивное представление о том, как ослабить, примените одну или несколько итераций прямого цикла и посмотрите, что перестает быть истинным в имеющейся у вас формуле.
начните с того, что вы хотите (постусловия), и усиливайте, пока не получите индуктивный инвариант. Чтобы получить интуитивное представление о том, как усилить, примените одну или несколько итераций цикла в обратном направлении и посмотрите, что нужно добавить, чтобы можно было вывести постусловие.
Если вы хотите, чтобы компьютер помогал вам в практике, я могу порекомендовать плагин дедуктивной проверки Jessie для программ на языке C из Frama-C . Есть и другие, особенно для аннотаций Java и JML, но я менее знаком с ними. Опробовать инварианты, о которых вы думаете, гораздо быстрее, чем работать, если они работают на бумаге. Я должен отметить, что проверка того, что свойство является индуктивным инвариантом, также неразрешима, но современные автоматические средства доказательства отлично справляются со многими простыми примерами. Если вы решили пойти по этому пути, возьмите как можно больше из списка: Alt-ergo, Simplify, Z3.
С дополнительной (и немного сложной в установке) библиотекой Apron, Джесси может также автоматически вывести некоторые простые инварианты .
Я не думаю, что это легко автоматизировать. Из вики:
Из-за фундаментального сходства циклов и рекурсивных программ, доказательство частичной корректности циклов с помощью инвариантов очень похоже на доказательство корректности рекурсивных программ с помощью индукции. Фактически, инвариант цикла часто является индуктивным свойством, которое нужно доказать для рекурсивной программы, эквивалентной данному циклу.
Сгенерировать инварианты цикла на самом деле тривиально. true - это, например, хороший вариант. Он выполняет все три свойства, которые вы хотите:
- Сохраняется до входа в цикл
- Сохраняется после каждой итерации
- Сохраняется после завершения цикла
Но то, что вам нужно, вероятно, самое сильное инвариант цикла. Однако найти самый сильный инвариант петли иногда бывает даже неразрешимой задачей. См. Статью Неадекватность инвариантов вычислимых циклов .
Существует ряд эвристик для поиска инвариантов петель. Одна хорошая книга об этом - «Программирование в 1990-е годы» Эда Коэна. Речь идет о том, как найти хороший инвариант, манипулируя постусловием вручную. Примеры: заменить константу переменной, усилить инвариант, ...