Установка инструментов

Для начала установите Git и OCaml - например, в Ubuntu:

sudo apt-get install git ocaml

Затем установите менеджер пакетов OPAM согласно его официальной документации. Например, для установки в /usr/local/bin с помощью бинарного инсталлятора:

wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh 
chmod +x opam_installer.sh
sudo ./opam_installer.sh /usr/local/bin

Инициализируйте OPAM:

opam init --comp 4.02.1 
eval `opam config env`

Добавьте OPAM-репозиторий Astraver в список репозиториев OPAM:

opam repo add astraver https://forge.ispras.ru/git/astraver.opam-repository.git

Установите внешние зависимости:

sudo apt-get install $(opam install -e ubuntu jessie2)

Соберите и установите плагин Jessie2 для Frama-C (сама Frama-C будет установлена автоматически; параметр -j 4 опционален и позволяет ускорить сборку на многоядерной машине):

opam install -j 4 jessie2

Установите платформу дедуктивной верификации Why3 и ее зависимости:

sudo apt-get install $(opam install -e ubuntu why3)
opam install -j 4 why3

Кроме того, для работы инструментов нужны SMT-солверы - например, Alt-Ergo (также поддерживаются Z3, CVC4 и другие). Alt-Ergo может быть установлен из OPAM:

opam install alt-ergo altgr-ergo satML-plugin

После установки нужно обновить настройки солверов и плагинов Why3:

why3 config --detect-provers --detect-plugins