Это команда why-dp, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
почему - многоязычный инструмент проверки с несколькими программами проверки
СИНТАКСИС
зачем [ кредита ] файлов
ОПИСАНИЕ
зачем это инструмент проверки. Он принимает аннотированные программы в качестве входных данных (в синтаксисе ML или C) и
выводит условия проверки для нескольких помощников пруфа (Coq, PVS, HOL Light, Mizar)
и процедуры принятия решений (haRVey, Simplify).
ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ
-h Помощь. Дает вам полный список параметров командной строки.
АВТОРЫ
Жан-Кристоф Филлиатр <[электронная почта защищена]>
Используйте why-dp в Интернете с помощью сервисов onworks.net
