Este é o comando cafeobj que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas múltiplas estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online de Windows ou emulador online de MAC OS
PROGRAMA:
NOME
cafeobj - especificação algébrica e linguagem de programação
SINOPSE
cafeobj [OPÇÃO] ... [ARQUIVOS] ...
DESCRIÇÃO
Inicia o CaféOBJ intérprete.
CaféOBJ é uma linguagem de especificação formal mais avançada que herda muitos recursos avançados
recursos (por exemplo, sintaxe mix-fix flexível, sistema de digitação poderoso e claro com ordenação
classificações, módulos paramétricos e visualizações para instanciar os parâmetros e módulo
expressões, etc.) da linguagem de especificação algébrica OBJ (ou mais exatamente OBJ3).
CafeOBJ é uma linguagem para escrever especificações formais (ou seja, matemáticas) de modelos para
ampla variedade de softwares e sistemas e verificação de propriedades deles. CaféOBJ
implementa lógica equacional reescrevendo e pode ser usado como um poderoso teorema interativo
sistema de prova. Os especificadores também podem escrever pontuações de prova no CafeOBJ e fazer provas por
executando as pontuações da prova.
CafeOBJ possui semântica lógica rigorosa de última geração baseada em instituições. O CaféOBJ
cubo mostra a estrutura das várias lógicas subjacentes à combinação dos vários
paradigmas implementados pela linguagem. As pontuações de prova no CafeOBJ também são baseadas em
semântica rigorosa baseada na instituição e pode ser construída usando um conjunto completo de provas
regras.
OPÇÕES
Existem duas classes de opções. As primeiras são opções para cafeobj roteiro de wrapper
que permite selecionar o interpretador Common Lisp subjacente e ajustar o caminho de pesquisa
parâmetros.
-motor NOME
seleciona o mecanismo lisp comum subjacente. Se não for fornecido, o primeiro selecionado
durante o tempo de construção é usado.
-list-motores
lista todos os motores LISP comuns disponíveis
-wrapper-libpath PATH
define o caminho onde os dumps de memória dos interpretadores lisp são encontrados
-wrapper-sharepath PATH
define o caminho onde os arquivos de inicialização CafeOBJ são pesquisados
O seguinte conjunto de opções é direcionado diretamente ao intérprete CafeOBJ:
-Socorro imprimir uma mensagem de ajuda
-q não carregue o arquivo de inicialização do usuário
-lote executar em modo lote
-p PATH
fornece os módulos de definição do arquivo prelúdio padrão
+p PATH
carregar arquivo de prelúdio adicional
-l LISTA DIR
definir lista de nomes de caminho para o caminho de pesquisa do módulo, separados por dois pontos
+l LISTA DIR
adiciona uma lista de nomes de caminho para o caminho de pesquisa do módulo
ARQUIVOS arquivos que são carregados no momento da inicialização em ordem.
Use cafeobj online usando serviços onworks.net