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

Question

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

Можно ли даже доказать, что Z3 верен, используя Z3?

Более теоретически, возможно ли доказать, что инструмент X является правильным, используя сам X?

Answer 1

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

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

После того, как мы договоримся о том, что мы должны доказать, мы должны создать модели семантики языка времени выполнения (C ++ в случае Z3)и т. д. Затем инструмент (он же верификатор) используется для преобразования фактического кода в набор формул, который мы должны проверить с помощью средства проверки теорем, такого как Z3.Нам нужен верификатор, потому что Z3 не «понимает» C ++.Верифицирующий компилятор C ( VCC ) является примером такого рода инструмента.Обратите внимание, что подтверждение правильности Z3 с использованием этого подхода не дает однозначной гарантии того, что Z3 действительно является правильным, поскольку наши модели могут быть неверными, верификатор может быть неправильным, Z3 может быть неправильным и т. Д.

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

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

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

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

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

Answer 2

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

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

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

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

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

Редактировать через 5 лет :

На самом деле аргумент проще, чем теорема Гёделя о неполноте.

Допустим, Z3 верен, если он возвращает UNSAT только для неудовлетворительных формул.

Предположим, мы находим формулу A, такую, что если Aнеудовлетворительно, тогда Z3 является правильным (и мы каким-то образом доказали это соотношение).

Мы можем передать эту формулу Z3, но

1. , если Z3 возвращает UNSAT, это может быть потому, что Z3исправить или из-за ошибки в Z3.Поэтому мы ничего не проверяли.
2. , если Z3 возвращает SAT и контрмодель, мы могли бы найти ошибку в Z3, проанализировав модель
3. , иначе мы ничего не знаем.

Таким образом, мы можем использовать Z3, чтобы находить ошибки в Z3 и повышать достоверность в отношении Z3 (до чрезвычайно высокого уровня), но не для формальной проверки.