Dies ist der Befehl „cafeobj“, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
cafeobj – algebraische Spezifikation und Programmiersprache
ZUSAMMENFASSUNG
Cafeobj [zur Auswahl]... [DATEIEN] ...
BESCHREIBUNG
Startet die CafeOBJ Dolmetscher.
CafeOBJ ist eine am weitesten fortgeschrittene formale Spezifikationssprache, die viele fortgeschrittene Merkmale erbt
Funktionen (z. B. flexible Mix-Fix-Syntax, leistungsstarkes und übersichtliches Typisierungssystem mit geordneter
Sortierungen, Parametermodule und Ansichten zum Instanziieren der Parameter und Module
Ausdrücke usw.) aus der algebraischen Spezifikationssprache OBJ (oder genauer OBJ3).
CafeOBJ ist eine Sprache zum Schreiben formaler (dh mathematischer) Spezifikationen von Modellen für
verschiedenster Software und Systeme sowie deren Eigenschaften überprüfen. CafeOBJ
implementiert Gleichungslogik durch Umschreiben und kann als leistungsstarker interaktiver Satz verwendet werden
Prüfsystem. Planer können auch in CafeOBJ Korrekturbewertungen schreiben und Korrekturen durchführen
Durchführen der Beweisergebnisse.
CafeOBJ verfügt über eine hochmoderne, strenge logische Semantik, die auf Institutionen basiert. Das CaféOBJ
Cube zeigt die Struktur der verschiedenen Logiken, die der Kombination der verschiedenen zugrunde liegen
Paradigmen, die von der Sprache implementiert werden. Die Proof-Scores in CafeOBJ basieren ebenfalls auf
Institutionsbasierte strenge Semantik und kann unter Verwendung eines vollständigen Beweissatzes konstruiert werden
Regeln.
OPTIONAL
Es gibt zwei Klassen von Optionen. Die ersten sind Optionen für Cafeobj Wrapper-Skript
Dies ermöglicht die Auswahl des zugrunde liegenden Common Lisp-Interpreters und die Anpassung des Suchpfads
Parameter.
-Motor NAME/FUNKTION
Wählt die zugrunde liegende Common-Lisp-Engine aus. Wenn nicht angegeben, wird der erste ausgewählt
während der Build-Zeit verwendet wird.
-list-engines
listet alle verfügbaren gängigen Lisp-Engines auf
-wrapper-libpath PATH
Legt den Pfad fest, in dem Speicherauszüge der Lisp-Interpreter gefunden werden
-wrapper-sharepath PATH
legt den Pfad fest, in dem CafeOBJ-Initialisierungsdateien gesucht werden
Die folgenden Optionen richten sich direkt an den CafeOBJ-Interpreter:
-Hilfe Drucken Sie eine Hilfemeldung
-q Laden Sie die Initialisierungsdatei des Benutzers nicht
-Charge im Batch-Modus ausführen
-p PATH
Gibt die standardmäßigen Prelude-Dateidefinitionsmodule an
+p PATH
Laden Sie die zusätzliche Prelude-Datei
-l DIR-LISTE
Liste der Pfadnamen für den Modulsuchpfad festlegen, durch Doppelpunkte getrennt
+l DIR-LISTE
Fügt eine Liste mit Pfadnamen für den Modulsuchpfad hinzu
DATEIEN Dateien, die beim Start geladen werden, der Reihe nach.
Nutzen Sie Cafeobj online über die Dienste von onworks.net
