Jest to polecenie cafeobj, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online Windows lub emulator online MAC OS
PROGRAM:
IMIĘ
cafeobj - specyfikacja algebraiczna i język programowania
STRESZCZENIE
kawiarniaobj [OPCJA]... [AKTA] ...
OPIS
Rozpoczyna KawiarniaOBJ interpretator.
KawiarniaOBJ jest najbardziej zaawansowanym językiem specyfikacji formalnej, który dziedziczy wiele zaawansowanych
funkcje (np. elastyczna składnia mix-fix, potężny i przejrzysty system typowania z zamówionym
sortuje, parametryczne moduły i widoki do tworzenia instancji parametrów i modułu
wyrażenia, itp.) z języka specyfikacji algebraicznej OBJ (lub dokładniej OBJ3).
CafeOBJ to język do zapisywania formalnych (tj. matematycznych) specyfikacji modeli dla
szeroka gama oprogramowania i systemów oraz weryfikacja ich właściwości. KawiarniaOBJ
implementuje logikę równań poprzez przepisywanie i może być używany jako potężne interaktywne twierdzenie
system dowodzenia. Specyfikatory mogą zapisywać wyniki sprawdzające również w CafeOBJ i przeprowadzać korekty przez
wykonanie ocen próbnych.
CafeOBJ posiada najnowocześniejszą rygorystyczną semantykę logiczną opartą na instytucjach. KawiarniaOBJ
kostka pokazuje strukturę różnych logik leżących u podstaw kombinacji różnych
paradygmaty realizowane przez język. Wyniki dowodu w CafeOBJ są również oparte na
rygorystyczna semantyka oparta na instytucjach i może być skonstruowana przy użyciu pełnego zestawu dowodów
zasady.
OPCJE
Istnieją dwie klasy opcji. Pierwsze to opcje dla kawiarniaobj skrypt opakowujący
który pozwala wybrać bazowy interpreter Common Lisp i dostosować ścieżkę wyszukiwania
parametry.
-silnik IMIĘ
wybiera podstawowy wspólny aparat lisp. Jeśli nie podano, pierwszy wybrany
w czasie kompilacji jest używany.
-lista-silników
zawiera listę wszystkich dostępnych popularnych silników lisp
-wrapper-libpath PATH
ustawia ścieżkę, w której znajdują się zrzuty pamięci interpreterów lisp
-wrapper-sharepath PATH
ustawia ścieżkę, w której przeszukiwane są pliki inicjujące CafeOBJ
Poniższy zestaw opcji jest skierowany bezpośrednio do interpretera CafeOBJ:
-Pomoc wydrukuj wiadomość pomocy
-q nie ładuj pliku inicjującego użytkownika
-seria uruchomić w trybie wsadowym
-p PATH
daje standardowy plik preludium definiujący moduły
+p PATH
załaduj dodatkowy plik preludium
-l DIR-LISTA
ustaw listę nazw ścieżek dla ścieżki wyszukiwania modułu, oddzielonych dwukropkami
+l DIR-LISTA
dodaje listę ścieżek do ścieżki wyszukiwania modułu
AKTA pliki, które są ładowane w czasie uruchamiania w kolejności.
Korzystaj z cafeobj online, korzystając z usług onworks.net
