Este é o comando alt-ergo que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas várias estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS
PROGRAMA:
NOME
Alt-Ergo - Um provador automático de teoremas dedicado à verificação do programa
SINOPSE
alternativo [ opções ] lima
DESCRIÇÃO
Alt-Ergo é um provador automático de teoremas. Leva como entradas um polimórfico arbitrário e
a fórmula de primeira ordem multi-classificada escrita é uma sintaxe por quê.
OPÇÕES
-h Ajuda. Fornece a lista completa de opções de linha de comando.
EXEMPLOS
Uma teoria de matrizes funcionais com índices inteiros. Esta teoria fornece um tipo embutido
('a,' b) farray e uma sintaxe embutida para manipular matrizes.
Por exemplo, dado um tipo de dados abstrato tau e uma matriz funcional t do tipo (int,
tau) farray declarado da seguinte forma:
digite tau
t lógico: (int, tau) farray
As expressões:
t [i] denota o valor armazenado em t no índice i
t [i1 <-v1, ..., em <-vn] denota uma matriz que armazena os mesmos valores de t para cada
índice exceto possivelmente i1, ..., in, onde armazena o valor v1, ..., vn. Esta expressão
é equivalente a ((t [i1 <-v1]) [i2 <-v2]) ... [em <-vn].
Exemplos.
t [0 <-v] [1 <-w]
t [0 <-v, 1 <-w]
t [0 <-v, 1 <-w] [1]
Uma teoria dos tipos de enumeração.
Por exemplo, um tipo de enumeração t com construtores A, B, C é definido como segue
:
tipo t = A | B | C
O que significa que todos os valores do tipo t são iguais a A, B ou C. E que todos
esses construtores são distintos.
Uma teoria de registros polimórficos.
Por exemplo, um tipo de registro polimórfico 'em com dois rótulos aeb do tipo' a e
int, respectivamente, é definido como segue:
digite 'em = {a:' a; b: int}
As expressões {a = 4; b = 5} e {r com b = 3} denotam registros, enquanto o ponto
a notação ra é usada para acessar os rótulos.
Alt-Ergo (v.> = 0.95) permite que o usuário force o tipo de termos usando a sintaxe :
. O exemplo abaixo ilustra o uso desse novo recurso.
digite 'uma lista
lógica nula: lista 'b
lógica f: 'c lista -> int
objetivo g1: f (nulo) = f (nulo) (* não é válido porque as duas instâncias de nulo podem ter
tipos diferentes *)
objetivo g2: f (nulo: 'lista d) = f (nulo:' lista d) (* válido *)
MEIO AMBIENTE VARIÁVEIS
ERGOLIB
Caminho alternativo para a biblioteca Alt-Ergo
AUTORES
Sylvain Conchon <[email protegido]> e Evelyne Contejean <[email protegido]>
Use alt-ergo online usando serviços onworks.net
