Questo è il comando cafeobj che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici postazioni di lavoro online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
cafeobj - specifica algebrica e linguaggio di programmazione
SINOSSI
cafeobj [OPZIONE]... [FILE] ...
DESCRIZIONE
inizia il CaféOBJ interprete.
CaféOBJ è un linguaggio di specifica formale più avanzato che eredita molti avanzati
caratteristiche (ad esempio sintassi mix-fix flessibile, sistema di digitazione potente e chiaro con ordinato
ordinamenti, moduli parametrici e viste per istanziare i parametri e modulo
espressioni, ecc.) dal linguaggio di specifica algebrica OBJ (o più esattamente OBJ3).
CafeOBJ è un linguaggio per scrivere specifiche formali (cioè matematiche) di modelli per
un'ampia varietà di software e sistemi e verificarne le proprietà. CafeOBJ
implementa la logica equazionale riscrivendo e può essere usato come un potente teorema interattivo
sistema dimostrativo. Gli specificatori possono scrivere i punteggi delle prove anche in CafeOBJ e fare prove di
l'esecuzione dei punteggi di prova.
CafeOBJ ha una semantica logica rigorosa all'avanguardia basata sulle istituzioni. Il CaffèOBJ
cubo mostra la struttura delle varie logiche sottese alla combinazione delle varie
paradigmi implementati dal linguaggio. Anche i punteggi delle prove in CafeOBJ si basano su
semantica rigorosa basata sull'istituzione e può essere costruita utilizzando un set completo di prove
regole.
VERSIONI
Ci sono due classi di opzioni. Le prime sono le opzioni per il cafeobj script wrapper
che consente di selezionare l'interprete Common Lisp sottostante e di regolare il percorso di ricerca
parametri.
-motore NOME
seleziona il motore lisp comune sottostante. Se non dato, il primo selezionato
durante il tempo di costruzione viene utilizzato.
-lista-motori
elenca tutti i motori lisp comuni disponibili
-wrapper-libpath PERCORSO
imposta il percorso in cui si trovano i dump della memoria degli interpreti lisp
-wrapper-condivisione percorso PERCORSO
imposta il percorso in cui vengono cercati i file di inizializzazione CafeOBJ
Il seguente set di opzioni è diretto direttamente all'interprete CafeOBJ:
-Aiuto stampa un messaggio di aiuto
-q non caricare il file di inizializzazione dell'utente
-lotto eseguire in modalità batch
-p PERCORSO
fornisce il file di preludio standard che definisce i moduli
+p PERCORSO
carica un file di preludio aggiuntivo
-l ELENCO DIR
imposta l'elenco dei percorsi per il percorso di ricerca del modulo, separati da due punti
+l ELENCO DIR
aggiunge un elenco di percorsi per il percorso di ricerca del modulo
FILE file che vengono caricati al momento dell'avvio in ordine.
Usa cafeobj online utilizzando i servizi onworks.net
