При использовании формальных аспектов для создания некоторого кода существует общий метод определения инварианта цикла или он будет полностью отличаться в зависимости от проблемы?Каков наилучший способ определения инварианта цикла?
Уже указано, что одна и та же петля может иметь несколько инвариантов и что Расчетность против вас. Это не значит, что вы не можете попробовать.
Вы, на самом деле, ищет индуктивный инвариантного: слово инвариантного также может быть использован для свойства, которое истинно на каждой итерации, но для которых он не достаточно, чтобы знать, что он проведет на одной итерации выведите, что он держится на следующем. Если I является индуктивным инвариантом, то любое последствие I является инвариантом, но не может быть индуктивным инвариантом.
Возможно, вы пытаетесь получить индуктивный инвариант, чтобы доказать определенное свойство (пост-условие) цикла в некоторых определенных обстоятельствах (предварительные условия).
Есть два эвристики, которые работают достаточно хорошо:
начать с того, что у вас есть (предварительные условия), и ослабить, пока вы не индуктивный инвариант. Чтобы получить интуицию, как ослабить, примените одну или несколько итераций цикла вперед и посмотрите, что перестает быть истинным в формуле, которую вы имеете.
начните с того, что вы хотите (пост-условия) и укрепите, пока не получите индуктивный инвариант. Чтобы получить интуицию, как усилить, примените одну или несколько итераций цикла назад и посмотрите, что нужно добавить, чтобы можно было вывести пост-состояние.
Если вы хотите, чтобы компьютер, чтобы помочь вам в вашей практике, я могу рекомендовать Jessie дедуктивной верификации плагин для программ С Frama-C. Есть и другие, особенно для Java и JML-аннотаций, но я с ними менее знаком. Выискивание инвариантов, о которых вы думаете, намного быстрее, чем разработка, если они работают на бумаге. Я должен отметить, что проверка того, что свойство является индуктивным инвариантом, также неразрешима, но современные автоматические прожекторы отлично справляются со многими простыми примерами. Если вы решите пойти по этому маршруту, получите в списке столько, сколько вы можете: Alt-ergo, Simplify, Z3.
С дополнительной (и немного сложной в установке) библиотекой Apron, Jessie также может infer some simple invariants automatically.
Не думаю, что автоматизировать это легко. Из вики:
Из-за фундаментальное сходство петель и рекурсивных программ, доказывающие частичную правильность петель с инвариантами очень похож на доказав правильность рекурсивных программ с помощью индукции. На самом деле, инвариант цикла часто является индуктивным свойством, нужно доказать рекурсивную программу, эквивалентную данному циклу.
Спасибо, я не хочу автоматизировать его, хотя это просто для ручек и бумажных упражнений, где мне нужно найти инварианты цикла. Думаю, это просто практика. – filinep
На самом деле тривиально создавать инварианты цикла. true является хорошим, например. Он выполняет все три свойства, которые вы хотите:
Но что вы после этого, вероятно, сильнейший цикл инвариант. Однако поиск наиболее сильного инварианта цикла иногда представляет собой задание unesableable. См. Статью Неадекватность инвариантов вычислимых циклов.
«Правда» слаба. Я думаю, вы имеете в виду «вы после * сильного * цикла инвариант». Ваш ответ поднял хороший момент, но я бы сказал, что обычно нужно «любой индуктивный инвариант достаточно сильный, чтобы доказать свойство, которое имеет в виду». Самый сильный инвариант цикла может не существовать (если существует бесконечность переменных, добавление «и x '= x» для нового x к инварианту, строит более сильный инвариант) и может быть громоздким. –
Что касается «слабых», вы правы, конечно. Я перепутал его! (Я думал об этом как «истина слаба, так как она ничего не подразумевает»). Ответ обновлен. Второй момент кажется мне немного искусственным. Вы говорите, что этого не существует, потому что для его записи потребуется бесконечное пространство? – aioobe
Ну, в большинстве логик формула представляет собой конечную совокупность символов, и я думаю, что некоторые мета-теоремы не будут истинными, если вы допустили бесконечные сборки, даже ограничивая себя регулярными сборками, которые можно описать конечно. Поэтому вы должны быть осторожны. Оставляя эту нитику в стороне (в ACSL вы можете указать инвариантность бесконечных переменных в конечном случае, например), я имел в виду, что самый сильный инвариант может быть намного сложнее, чем необходимо. –
Существует множество эвристик для поиска инвариантов цикла. Одна хорошая книга об этом - «Программирование в 1990-х годах» Эд Коэна. Речь идет о том, как найти хороший инвариант, манипулируя постусловием вручную. Примерами являются: замена константы на переменную, усиление инварианта, ...
Я написал о написании инвариантов цикла в своем блоге, см. Verifying Loops Part 2. Инварианты, необходимые для проверки правильности петли, обычно состоят из 2 частей:
(2) прост. Чтобы получить (1), начните с предиката, выражающего желаемое состояние после завершения. Скорее всего, он содержит «forall» или «существует» по некоторому диапазону данных. Теперь измените границы «forall» или «exist», чтобы (a) они зависели от переменных, модифицированных циклом (например, счетчики циклов) и (b), так что инвариант тривиально верен, когда цикл сначала вводится (обычно, делая диапазон «forall» или «exists» пустым).
Ну, вот оно. Идеальный ответ. +1 :) Хотя, вы когда-нибудь видели, что Simplify решила обязательство, что Alt-ergo или Z3 не удалось?:-) – aioobe
@aioobe В этой статье Simplify преуспевает, и на рис.1 есть обязательство с запрошенным свойством (оба Alt-ergo и Z3 сбой на нем). Все зависит от целевой программы, конечно :) http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf –
Aha, nice :-) первый, который я видел :) – aioobe