Why3 и стратегии запуска солверов

Why3 - это платформа для дедуктивной верификации. В связке с Frama-C используется как интерактивная среда для работы с доказательством условий верификации. Предоставляет среду интеграции для запуска различный автоматических и интерактивных доказателей, обрабатывает протоколы доказательств, предоставляет возможность применения различных трансформаций для логических формул (разбиения, подстановки, инверсии и т.д.).
Why3 - имеет внутренний язык конфигурации для стратегий запуска солверов. Что он позволяет делать? Запускать версии солверов с параметрами доступных памяти и времени, применять преобразования условий верификации. По большому счёту это всё.
К огромному сожалению, данный язык конфигурации нигде разработчиками не описан. Даже сама информация о наличии возможности применения стратегий довольно продолжительное время как-то специально не афишировалась. Всю информацию я почерпнул из исходных кодов.

Язык состоит из трёх команд: команда запуска солвера (call), команда применения трансормации формулы (transform), команда безусловного перехода по метке (goto). Эти три команды могут быть сокращены до одной буквы c, t, g. Также языком поддерживаются метки. Они аналогичны таковым в языке Си, в языке ассемблера.

Рассмотрим команды подробнее.

Goto

Команда безусловного перехода по метке. Имеет следующее строение:

goto <label>

Аналогична таковым в ассемблере и в языке Си. Метки ставятся следующим образом <label>: <command>. Метка exit является стандартной. Она обозначает конец стратегии.

Call

Команда запуска солвера. Имеет следующее строение:

call <solver>, <timelimit> <memlimit>

Где solver состоит из имени солвера, версии и специального обозначения способа запуска солвера (если он есть), которые указываются через запятую: <name>,<version>,<alternative>. Timelimit задаёт время на запуск солвера в секундах. Memlimit задаёт ограничение на память в мегабайтах.
Примеры:

c Alt-Ergo,0.95.2, 1 1000
c Alt-Ergo,0.95.2,-Em 1 1000
c CVC4,1.4,-trigs 1 1000

Семантика выполнения команды такова: запустить указанный солвер с определенными ограничениями по памяти и времени; если солвер доказывает условие верификации, то завершить выполнение стратегии; если солвер не может доказать условие верификации, то перейти к следующей команде.

Transform

Имеет следующее строение:

transform <transformation> <label>

Где transformation - одна из доступных трансформаций для условия верификации, например, inline_goal, introduce_premises, ... label - метка перехода для случая, когда трансформация успешно применилась. Если трансформация не применима, то будет выполняться следующая команда.
Примеры:

transform inline_goal L1
goto exit
L1: transform split_goal_wp exit

Примеры стратегий

Рассмотрим подробнее полноценные примеры стратегий.
Пример стратегии split:

[strategy]
name = "Split"
desc = "Split"
shortcut = "s"
code = "t split_goal_wp exit"

Поле name используется для отображения имени стратегии на кнопке в why3. Поле desc - описание стратегии, отображается при наведении указателя мыши на кнопку. shortcut - сокращение для клавиатуры. code - код стратегии на рассмотренном ранее языке.
В данном примере просто применяется трансформация split_goal_wp с меткой выхода exit. Если стратегия не может примениться она завершается ровно на той же метке завершения стратегии.

[strategy]
name = "Inline"
desc = "Inline All and Remove Triggers"
shortcut = "i"
code = "
t inline_all L1
L1: t remove_triggers exit"

Это пример применения двух последовательных трансформаций к условию верификации. По сути, просто объединение двух разных кнопок в одну.

[strategy]
name = "Cool"
desc = "My Very Cool Strategy"
shortcut = "mc"
code = "c Alt-Ergo,1.30, 1 1000"

Запуск солвера Alt-Ergo с ограничением по времени в одну секунду и по памяти в тысячу мегабайт.

[strategy]
name = "Mini Blaster"
desc = "[email protected] [email protected] blaster"
shortcut = "b"
code = "
start:
  c Alt-Ergo,1.30, 1 1000
  c CVC4,1.4, 1 1000
  t split_goal_wp start
  c Alt-Ergo,1.30, 10 4000
  c CVC4,1.4, 10 4000"

Пример более продвинутой стратегии. Она выглядит следующим образом:

  1. Запустить Alt-Ergo. Если он не справился, то перейти к шагу 2.
  2. Запустить CVC4. Если он не справился, то перейти в шагу 3.
  3. Подразбить формулу по конъюнктам для того, чтобы доказывать их по отдельности. Делает из одного условий верификации несколько более простых. Если удаётся подразбить формулу, то перейти к шагу 1, если нет, то к шагу 4. На новых целях после подразбиения запускается таже стратегия.
  4. Запустить Alt-Ergo с большим количеством памяти и времени, чем на шаге 1. Если он не справится, то перейти к шагу 5.
  5. Запустить CVC4 с большим количеством памяти и времени, чем на шаге 2. Если он не справится, то завершить запуск стратегии.

На каждом шаге (кроме 3-го), если солвер доказывает условие верифкации, то стратегия завершается с положительным результатом.

Comments

comments powered by Disqus