Когда команда прицела выполнена успешно, подтвердился ли мой контракт правильным?

Question

Когда перекрестие не находит контрпримеров, использовал ли он решатель Z3, чтобы доказать, что мой контракт выполняется?

В документы свидетельствуют о том, что отсутствие контрпример не гарантирует, что свойство имеет место, но в том, что только потому, что перевод или моделирование может быть неправильно?

Отказ от ответственности: я являюсь основным участником CrossHair (я просто использую переполнение стека как общедоступный способ записи ответов на вопросы, которые мне задавали ранее)

Answer 1

Помимо вероятных проблем с ненадлежащим моделированием, CrossHair не предоставляет эту гарантию.

CrossHair - крайне неполная система. Внутренне для каждого постусловия он генерирует три возможных результата: "подтверждено", "отклонено" и "неизвестно". Он производит вывод только для "отклоненного" случая; следовательно, отсутствие вывода не указывает на проверку утверждения.

Почему CrossHair работает именно так? Две причины:

1. CrossHair генерирует "неизвестное" для всех случаев, кроме самых тривиальных. Для большинства разработчиков различие между "неизвестным" и "подтвержденным" не имеет особого смысла. (по крайней мере, в настоящее время рефакторинг вашего кода, чтобы сделать его полностью доступным для изучения с помощью CrossHair, будет невозможным или уродливым) Обратите внимание, однако, что CrossHair будет пытаться выполнить множество путей, прежде чем выдаст "неизвестный" результат - результат по-прежнему является некоторым свидетельством того, что условие выполняется.
2. Различие подтвержденных и неизвестных со временем будет очень нестабильным. CrossHair разработан с нуля, чтобы развиваться. В среднем решатели SMT станут лучше. CrossHair поправится. Но в среднем оба поправятся; в отдельных случаях ситуация могла ухудшиться. Чтобы избежать опасений по поводу регрессии подтвержденного и неизвестного, это различие по умолчанию скрыто.

Лучше всего думать о CrossHair как о тестере нечеткости с помощью решателя.

С учетом всего сказанного, если вы все же хотите увидеть, какие свойства можно подтвердить, вы можете запросить этот вывод с помощью специальной опции "сообщить обо всем": crosshair check --report_all [TARGET].