Виртуальная машина для выполнения задания практикума

Для выполнения практических заданий вам потребуется (как минимум) инструмент Krakatoa (вместе Why3) и солверы. Вы можете попробовать установить их вручную (например, собрав из исходников, не забыв про патчи) или воспользоваться виртуальной машиной со всем необходимым предустановленным ПО.

Вы можете скачать виртуальную машину (версия от 11 ноября 2013 года) по следующим ссылкам:

Развёртывание виртуальной машины

  1. Скачать, установить и запустить VirtualBox.
  2. В меню Файл выбрать пункт "Импорт конфигураций...", выбираете файл со скаченной с сайта виртуальной машиной, проверяете параметры машины, нажимаете кнопку "Импорт".

Использование виртуальной машины

В этой виртуальной машине установлена ОС Gentoo Linux. При загрузке запускается графический режим с автовходом в аккаунт student (пароль student). В качестве терминала следует использовать xterm, в качестве файлового менеджера pcmanfm, в качестве текстового редактора vim, nano, leafpad (этот - в графическом режиме). Установлен веб-браузер Firefox. Установлена java и среда разработки Eclipse. Установлен инструмент Krakatoa, Why3 и солверы Alt-Ergo, CVC4, Z3, Gappa.
Чтобы воспользоваться инструментом Krakatoa, нужно написать текстовый файл (файлы) с исходными текстами на Java, снабженными спецификационными комментариями, и в терминале дать команду "krakatoa имена-файлов". Если в файлах есть ошибки, krakatoa их напишет. Если ошибок не было, запустится графическая оболочка Why3IDE, в которой надо сначала щелкнуть по утверждению в центральной части оболочки, затем щелкнуть на кнопку солвера (например, Alt-Ergo). Если солвер смог доказать утверждение, рядом с утверждением появится радостный зеленый кружок. Если солвер не уложился во время доказательства, рядом с утверждением появится красный значок часов. Если солвер уложился во время, но ответил unknown, рядом с утверждением появится песочного цвета кружок со знаком вопроса. Если солвер "упал" во время доказательства, рядом с утверждением появится черный значок бомбы. Если солвер как раз сейчас доказывает утверждение, рядом с утверждением будет фиолетовый значок с треугольником как Play в магнитофонах. Если солвер еще не запускался, но это планируется сделать, рядом с утверждением нарисован маленький фиолетовый кружок. Подробнее про интерфейс Why3IDE и инструмент Krakatoa можно прочитать на сайте этого инструмента.
Свои замечания о проблемах с виртуальной машиной посылайте, пожалуйста, Евгению Корныхину.
Последнее изменение: понедельник, 11 ноября 2013, 18:15