Il s'agit de la commande cafeobj qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
cafeobj - spécification algébrique et langage de programmation
SYNOPSIS
caféobj [OPTION]... [DES DOSSIERS] ...
DESCRIPTION
Démarre le CaféOBJ interprète.
CaféOBJ est un langage de spécification formelle le plus avancé qui hérite de nombreux
fonctionnalités (par exemple, syntaxe mix-fix flexible, système de frappe puissant et clair avec
tris, modules paramétriques et vues pour instancier les paramètres, et module
expressions, etc.) du langage de spécification algébrique OBJ (ou plus exactement OBJ3).
CafeOBJ est un langage pour écrire des spécifications formelles (c'est-à-dire mathématiques) de modèles pour
grande variété de logiciels et de systèmes, et vérifier leurs propriétés. CaféOBJ
implémente la logique équationnelle par réécriture et peut être utilisé comme un puissant théorème interactif
système de preuve. Les spécificateurs peuvent également écrire des partitions de preuve dans CafeOBJ et faire des preuves en
exécuter les scores de preuve.
CafeOBJ a une sémantique logique rigoureuse de pointe basée sur les institutions. Le CaféOBJ
cube montre la structure des différentes logiques qui sous-tendent la combinaison des différents
paradigmes mis en œuvre par le langage. Les scores de preuve dans CafeOBJ sont également basés sur
sémantique rigoureuse basée sur l'institution, et peut être construit à l'aide d'un ensemble complet de preuves
règles.
OPTIONS
Il existe deux classes d'options. Les premiers sont des options pour le caféobj script wrapper
qui permet de sélectionner l'interpréteur Common Lisp sous-jacent et d'ajuster le chemin de recherche
paramètres.
-moteur Nom
sélectionne le moteur lisp commun sous-jacent. Si non donné, le premier sélectionné
pendant le temps de construction est utilisé.
-liste-moteurs
répertorie tous les moteurs de lisp courants disponibles
-wrapper-libpath PATH
définit le chemin où se trouvent les vidages de mémoire des interpréteurs lisp
-wrapper-sharepath PATH
définit le chemin où les fichiers d'initialisation CafeOBJ sont recherchés
L'ensemble d'options suivant s'adresse directement à l'interpréteur CafeOBJ :
-Aide imprimer un message d'aide
-q ne charge pas le fichier d'initialisation de l'utilisateur
-grouper exécuter en mode batch
-p PATH
donne le fichier prélude standard définissant les modules
+p PATH
charger un fichier de prélude supplémentaire
-l LISTE DIR
définir la liste des chemins d'accès pour le chemin de recherche de module, séparés par des deux-points
+l LISTE DIR
ajoute une liste de chemin d'accès pour le chemin de recherche de module
DES DOSSIERS fichiers qui sont chargés au démarrage dans l'ordre.
Utilisez cafeobj en ligne en utilisant les services onworks.net
