Este es el comando cafeobj que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
cafeobj - lenguaje de programación y especificación algebraica
SINOPSIS
cafeobj [OPCIÓN] ... [ARCHIVOS] ...
DESCRIPCIÓN
Inicia el CaféOBJ Interprete.
CaféOBJ es un lenguaje de especificación formal más avanzado que hereda muchos
características (p. ej., sintaxis mix-fix flexible, sistema de escritura potente y claro con
clasificaciones, módulos paramétricos y vistas para instanciar los parámetros, y módulo
expresiones, etc.) del lenguaje de especificación algebraica OBJ (o más exactamente OBJ3).
CafeOBJ es un lenguaje para escribir especificaciones formales (es decir, matemáticas) de modelos para
una amplia variedad de software y sistemas, y verificar las propiedades de los mismos. CafeOBJ
Implementa la lógica de las ecuaciones mediante la reescritura y se puede utilizar como un poderoso teorema interactivo.
probando sistema. Los especificadores pueden escribir puntuaciones de prueba también en CafeOBJ y hacer pruebas por
ejecutar las puntuaciones de prueba.
CafeOBJ tiene una semántica lógica rigurosa de última generación basada en instituciones. El CafeOBJ
El cubo muestra la estructura de las diversas lógicas subyacentes a la combinación de las diversas
paradigmas implementados por el lenguaje. Las puntuaciones de prueba en CafeOBJ también se basan en
semántica rigurosa basada en la institución, y se puede construir utilizando un conjunto completo de pruebas
reglas.
CAMPUS
Hay dos clases de opciones. Las primeras son opciones para el cafeobj guión envoltorio
que permite seleccionar el intérprete Common Lisp subyacente y ajustar la ruta de búsqueda
parámetros.
-motor NOMBRE
selecciona el motor lisp común subyacente. Si no se da, el primero seleccionado
durante el tiempo de construcción se utiliza.
-lista-motores
enumera todos los motores lisp comunes disponibles
-wrapper-libpath TRAYECTORIA
establece la ruta donde se encuentran los volcados de memoria de los intérpretes lisp
-wrapper-sharepath TRAYECTORIA
establece la ruta donde se buscan los archivos de inicialización de CafeOBJ
El siguiente conjunto de opciones están dirigidas directamente al intérprete de CafeOBJ:
-ayuda imprimir un mensaje de ayuda
-q no cargue el archivo de inicialización del usuario
-lote ejecutar en modo por lotes
-p TRAYECTORIA
proporciona los módulos de definición de archivos de preludio estándar
+p TRAYECTORIA
cargar archivo de preludio adicional
-l LISTA DIR
Establecer lista de nombres de ruta para la ruta de búsqueda del módulo, separados por dos puntos
+l LISTA DIR
agrega una lista de nombre de ruta para la ruta de búsqueda del módulo
ARCHIVOS archivos que se cargan en el momento del inicio en orden.
Utilice cafeobj en línea utilizando los servicios de onworks.net
