Project

General

Profile

Инструкция по установке и настройке Rodin

Для установки Rodin выполните следующие действия:

  1. Установите Java Runtime Environment (JRE).
  2. Скачайте архив с Rodin (на данный момент актуальная версия - 3.4): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/
  3. Распакуйте архив в любом месте на жестком диске и запустите исполняемый файл rodin.
Перед использованием Rodin желательно установить два плагина:
  • SMT Solvers, позволяет использовать SMT-решатели для автоматического доказательства.
  • Atelier B Provers, набор дополнительных инструментов автоматического доказательства.

Для установки плагина SMT Solvers выполните следующие действия:

  1. Запустите Rodin и перейдите в раздел Help > Install New Software.
  2. В выпадающем меню Work with выберите Rodin.
  3. Появится на выбор несколько категорий с различными плагинами. Разверните категорию Prover Extensions и поставьте галку рядом с SMT Solvers. Нажмите Next.
  4. Проверьте, что все верно, и нажмите Next.
  5. Прочитайте и примите условия лицензионного соглашения. Затем нажмите кнопку Finish.
  6. Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажмите OK.
  7. Установка может занять некоторое время. По окончанию нажмите на Restart Now.
Установка Atelier B Provers почти не отличается от установки SMT Solvers Plug-in. Отличия:
  • На шаге номер 2 в выпадающем меню Work with нужно выбрать Atelier B Provers.
  • На шаге номер 3 нужно развернуть категорию Atelier B Provers и поставьте галочку рядом с Atelier B Provers.
После установки плагинов их нужно настроить. Для этого:
  1. Откройте окно настроек Rodin (пункт Window > Preferences в меню, или Rodin Platform > Preferences на macOS).
  2. В выпадающем списке меню выберите Event-B > Sequent Prover > Auto/Post Tactic.
  3. В разделе Auto-Tactics в выпадающем списке Tactic profile to be used for auto-tactics выберите Default Auto Tactic with SMT.
  4. В разделе Post-Tactics уберите галку напротив Enable post-tactic for proving.