Это команда cafeobj, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
cafeobj - язык алгебраической спецификации и программирования
СИНТАКСИС
кафеобъект [ВАРИАНТ] ... [FILES] ...
ОПИСАНИЕ
Запускает КафеOBJ переводчик.
КафеOBJ это наиболее продвинутый язык формальных спецификаций, унаследовавший многие продвинутые
функции (например, гибкий синтаксис смешанного исправления, мощная и понятная система ввода с упорядоченными
сортировки, параметрические модули и представления для создания экземпляров параметров, а также модуль
выражения и т. д.) из языка алгебраической спецификации OBJ (точнее, OBJ3).
CafeOBJ - это язык для написания формальных (т.е. математических) спецификаций моделей для
широкое разнообразие программного обеспечения и систем, а также проверка их свойств. КафеOBJ
реализует эквациональную логику путем переписывания и может использоваться как мощная интерактивная теорема
система доказывания. Спецификаторы могут писать оценки проверки также в CafeOBJ и делать доказательства с помощью
выполнение контрольных оценок.
CafeOBJ обладает современной строгой логической семантикой, основанной на институтах. КафеOBJ
куб показывает структуру различных логик, лежащих в основе комбинации различных
парадигмы, реализуемые языком. Доказательства в CafeOBJ также основаны на
строгая семантика, основанная на учреждении, и может быть построена с использованием полного набора доказательств
правила.
ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ
Есть два класса опций. Первые - это варианты кафеобъект скрипт-обёртка
что позволяет выбрать базовый интерпретатор Common Lisp и настроить путь поиска
параметры.
-движок ИМЯ
выбирает базовый общий движок lisp. Если не указан, выбран первый
во время сборки используется.
-лист-двигатели
перечисляет все доступные распространенные движки lisp
-wrapper-libpath PATH
устанавливает путь, по которому находятся дампы памяти интерпретаторов lisp
-wrapper-sharepath PATH
устанавливает путь, по которому ищутся файлы инициализации CafeOBJ
Следующий набор опций направлен непосредственно на интерпретатор CafeOBJ:
-Помощь распечатать справочное сообщение
-q не загружать файл инициализации пользователя
-партия запустить в пакетном режиме
-p PATH
дает стандартные модули определения файла прелюдии
+p PATH
загрузить дополнительный файл прелюдии
-l СПИСОК КАТАЛОГ
установить список путей для пути поиска модуля, разделенных двоеточиями
+l СПИСОК КАТАЛОГ
добавляет список путей для пути поиска модуля
FILES файлы, которые загружаются при запуске по порядку.
Используйте cafeobj онлайн с помощью сервисов onworks.net
