Кто-нибудь пытался доказать Z3 с самой Z3?

Ответ 1

Короткий ответ: "нет, никто не пытался доказать Z3, используя сам Z3": -)

Предложение "мы доказали правильность программы X" очень вводит в заблуждение. Основная проблема заключается в следующем: что значит быть правильным. В случае Z3 можно сказать, что Z3 является правильным, если, по крайней мере, он никогда не возвращает "sat" для неудовлетворительной проблемы и "unsat" для выполнимого. Это определение может быть улучшено за счет включения дополнительных свойств, таких как: Z3 не должен аварийно завершаться; функция X в Z3 API имеет свойство Y и т.д.

После того, как мы договоримся о том, что мы должны доказать, нам нужно создать модели среды выполнения, семантики языка программирования (С++ в случае Z3) и т.д. Затем инструмент (aka verifier) ​​используется для преобразования фактического кода в набор формул, которые мы должны проверять с помощью доказательства теоремы, такого как Z3. Нам нужен верификатор, потому что Z3 не "понимает" С++. Компилятор Verifying C (VCC) является примером такого инструмента. Обратите внимание, что проверка правильности Z3 с использованием этого подхода не дает окончательной гарантии того, что Z3 действительно прав, поскольку наши модели могут быть неправильными, верификатор может быть неправильным, Z3 может быть неправильным и т.д.

Чтобы использовать верификаторы, такие как VCC, нам нужно аннотировать программу со свойствами, которые мы хотим проверить, инвариантами цикла и т.д. Некоторые аннотации используются для определения того, какие фрагменты кода должны делать. Другие аннотации используются для "помощи/руководства" доказательства теоремы. В некоторых случаях количество аннотаций больше, чем проверяемая программа. Таким образом, процесс не является полностью автоматическим.

Другой проблемой является стоимость, процесс будет очень дорогим. Это было бы намного более трудоемким, чем внедрение Z3. Z3 имеет 300k строк кода, некоторые из этого кода основаны на очень тонких алгоритмах и трюках реализации. Еще одна проблема - техническое обслуживание, мы регулярно добавляем новые функции и улучшаем производительность. Эти изменения повлияют на доказательство.

Хотя стоимость может быть очень высокой, VCC используется для проверки нетривиальных фрагментов кода, таких как гипервизор Microsoft Hyper-V.

В теории любой верификатор для языка программирования X может быть использован для доказательства, если он также реализован на языке X. SpeС# verifier является примером такого инструмента. SpeС# реализован в SpeС#, и несколько частей SpeС# были проверены с использованием SpeС#. Обратите внимание, что SpeС# использует Z3 и предполагает, что он правильный. Конечно, это большое предположение.

Более подробную информацию об этих проблемах и приложениях Z3 можно найти на бумаге: http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf

Ответ 2

Нет, невозможно доказать, что нетривиальный инструмент верен с использованием самого инструмента. Это было в основном указано в Вторая теорема неполной неполноты Гёделя:

Для любой формально эффективно генерируемой теории T, включающей основные арифметические истины, а также некоторые истины о формальной доказуемости, если T включает в себя утверждение о своей собственной согласованности, то T несовместимо.

Так как Z3 включает арифметику, он не может доказать свою собственную согласованность.

Потому что это было упомянуто в комментарии выше: Даже если пользователь предоставляет инварианты, теорема Гёдельса все еще применяется. Это не вопрос вычислимости. Теорема утверждает, что такое доказательство не может существовать в согласованной системе.

Однако вы можете проверить части Z3 с Z3.