Что такое триггеры в Дафни / Буги?

Question

Я бездельничал в Дафни, не понимая триггеров. Возможно, в результате программы, которые я пишу, кажутся трудным временем для верификатора. Иногда я трачу кучу времени, возясь с доказательством, пытаясь убедить Дафни / Буги в том, что оно действительно; и когда я получаю что-то работающее, иногда это медленно проверяется (что серьезно ухудшает мою способность продолжать).

Трудно задать точный вопрос, потому что я не знаю, что это, я не знаю. Но давайте начнем с основ:

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

Answer 1

Понимание триггеров - определенно важная часть становления экспертом в Дафни!

Недавно мы открыли страницу с часто задаваемыми вопросами для Дафни, которая содержит довольно подробное описание триггеров. Я рекомендую вам начать с чтения этой части FAQ. (Остальная часть этого ответа предполагает, что вы сделали это.)

Одна вещь, которая не охвачена, это то, как триггеры выводятся. (Скоро я добавлю отредактированную версию этого ответа в FAQ.) На самом деле триггеры потенциально выводятся на двух разных уровнях: Dafny или Z3. Как правило, лучше, если триггер выведен на уровне Дафни, потому что более вероятно найти краткий триггер до того, как все детали кодирования от преобразования к Z3 будут задействованы. Однако, если Дафни не удается определить триггер, иногда Z3 все еще может сделать что-то полезное в качестве временного промежутка. (В таких случаях Дафни выдает предупреждение.)

Процедура вывода, используемая как Z3, так и Дафни, концептуально очень похожа. Дано количественное выражение forall x1, ..., xn :: e процедура вывода пытается найти подвыражения e которые включают только переменные, константы и неинтерпретированные функции / предикаты, так что каждый xi появляется в подвыражении. Например, в выражении

forall a, b :: P(a) && Q(a, b) ==> R(b)

выражение Q(a, b) является допустимым триггером, так как он упоминает все связанные переменные и не включает никаких интерпретируемых функций. Другой допустимый триггер - это набор выражений {P(a), R(b)}, Лучше ли один триггер или другой (или оба) зависит от контекста. Обычно Dafny выводит и использует все допустимые, максимально общие триггеры, поэтому в этом случае он выберет оба Q(a, b) а также {P(a), R(b)},

В общем, триггерный вывод Дафни работает, перечисляя все допустимые триггеры, просматривая все подвыражения e, Затем Dafny отфильтровывает триггеры, которые являются строго менее общими, чем другой допустимый триггер. Дафни выбирает все оставшиеся триггеры.

Для дополнительного чтения я рекомендую статью " Упрощение: проверка теорем для проверки программ " Детлефсом, Нельсоном и Саксом. Simplify был ранним SMT-решателем, который впервые использовал эвристическое использование триггеров для обработки квантификаторов. Раздел 5 вышеупомянутого документа описывает подход в технических деталях.