Понимание триггеров - определенно важная часть становления экспертом в Dafny!
Недавно мы открыли страницу часто задаваемых вопросов для Dafny, которая включает в себя довольно обширное описание триггеров.Я рекомендую вам начать с чтения этой части 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) является допустимым триггером, поскольку оно упоминает все связанные переменные и не включает никаких интерпретируемых функций.Другим допустимым триггером является set выражения {P(a), R(b)}.Лучше ли один триггер или другой (или оба) зависит от контекста.Обычно Dafny выводит и использует все допустимые, максимально общие триггеры, поэтому в этом случае он выберет Q(a, b) и {P(a), R(b)}.
Как правило, вывод триггера Дафни работает путем перечисления всех допустимых триггеров, просматривая все подвыражения e.Затем Dafny отфильтровывает триггеры, которые являются строго менее общими, чем другой допустимый триггер.Дафни выбирает все оставшиеся триггеры.
Для дополнительного чтения я рекомендую статью Упрощение: проверка теорем для проверки программ Детлефсом, Нельсоном и Саксом.Simplify был ранним SMT-решателем, впервые применившим эвристическое использование триггеров для обработки квантификаторов.Раздел 5 вышеприведенного документа описывает этот подход в технических деталях.