Це команда cafeobj, яку можна запустити у безкоштовного хостинг-провайдера OnWorks за допомогою однієї з наших безкоштовних онлайн-робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS
ПРОГРАМА:
ІМ'Я
cafeobj - алгебраїчна специфікація та мова програмування
СИНТАКСИС
cafeobj [ВАРІАНТ]... [ФАЙЛИ]...
ОПИС
Починає КафеOBJ перекладач.
КафеOBJ це найдосконаліша формальна мова специфікації, яка успадковує багато передових
функції (наприклад, гнучкий синтаксис mix-fix, потужна та зрозуміла система набору тексту з упорядкованим
sorts, параметричні модулі та представлення для створення екземплярів параметрів і модуль
вирази тощо) з мови алгебраїчних специфікацій OBJ (точніше OBJ3).
CafeOBJ — це мова для написання формальних (тобто математичних) специфікацій моделей для
широкий вибір програмного забезпечення та систем, а також перевірка їх властивостей. КафеOBJ
реалізує логіку рівнянь шляхом переписування та може використовуватися як потужна інтерактивна теорема
система доведення. Специфікатори можуть писати перевірочні оцінки також у CafeOBJ і виконувати перевірки
виконання пробних оцінок.
CafeOBJ має сучасну сувору логічну семантику, засновану на інститутах. Кафе OBJ
куб показує структуру різних логік, що лежать в основі поєднання різних
парадигми, реалізовані мовою. Доказові бали в CafeOBJ також базуються на
інституція базується на строгій семантиці та може бути створена за допомогою повного набору доказів
правила.
ВАРІАНТИ
Є два класи варіантів. Перші - це варіанти для cafeobj скрипт оболонки
що дозволяє вибрати базовий інтерпретатор Common Lisp і налаштувати шлях пошуку
параметри
- двигун ІМ'Я
вибирає основний движок Common Lisp. Якщо не вказано, перший вибраний
під час будівництва використовується час.
-спискові механізми
перераховує всі доступні загальні механізми lisp
-wrapper-libpath PATH
встановлює шлях, де знаходяться дампи пам'яті інтерпретаторів lisp
-wrapper-sharepath PATH
встановлює шлях, де шукаються файли ініціалізації CafeOBJ
Наступний набір параметрів спрямований безпосередньо на інтерпретатора CafeOBJ:
-допомога роздрукувати довідкове повідомлення
-q не завантажувати файл ініціалізації користувача
- партія працювати в пакетному режимі
-p PATH
надає стандартні модулі визначення файлу прелюдії
+p PATH
завантажити додатковий файл прелюдії
-l DIR-LIST
встановити список імен шляхів для шляху пошуку модуля, розділених двокрапками
+l DIR-LIST
додає список шляхів для шляху пошуку модуля
ФАЙЛИ файли, які завантажуються під час запуску в порядку.
Використовуйте cafeobj онлайн за допомогою сервісів onworks.net