Este es el comando alt-ergo 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
Alt-Ergo: un demostrador automático de teoremas dedicado a la verificación de programas
SINOPSIS
alt-ergo [ opciones ] presentar
DESCRIPCIÓN
Ergo alternativo es un demostrador automático de teoremas. Toma como entradas un polimórfico arbitrario y
La fórmula de primer orden con varios ordenamientos es una sintaxis similar a por qué.
OPCIONES
-h Ayudar. Le dará la lista completa de opciones de línea de comando.
EJEMPLOS
Una teoría de matrices funcionales con índices enteros. Esta teoría proporciona un tipo incorporado
('a,' b) farray y una sintaxis incorporada para manipular matrices.
Por ejemplo, dado un tipo de datos abstracto tau y una matriz funcional t de tipo (int,
tau) farray declaró lo siguiente:
tipo tau
lógica t: (int, tau) farray
Las expresiones:
t [i] denota el valor almacenado en t en el índice i
t [i1 <-v1, ..., en <-vn] denota una matriz que almacena los mismos valores que t para cada
index excepto posiblemente i1, ..., in, donde almacena el valor v1, ..., vn. Esta expresión
es equivalente a ((t [i1 <-v1]) [i2 <-v2]) ... [en <-vn].
Ejemplos.
t [0 <-v] [1 <-w]
t [0 <-v, 1 <-w]
t [0 <-v, 1 <-w] [1]
Una teoría de los tipos de enumeración.
Por ejemplo, un tipo de enumeración t con los constructores A, B, C se define de la siguiente manera
:
tipo t = A | B | C
Lo que significa que todos los valores de tipo t son iguales a A, B o C. Y que todos
estos constructores son distintos.
Una teoría de registros polimórficos.
Por ejemplo, un tipo de registro polimórfico 'at con dos etiquetas ayb de tipo' ay
int respectivamente se define de la siguiente manera:
escriba 'en = {a:' a; b: int}
Las expresiones {a = 4; b = 5} y {r con b = 3} denotan registros, mientras que el punto
la notación ra se utiliza para acceder a las etiquetas.
Alt-Ergo (v.> = 0.95) permite al usuario forzar el tipo de términos usando la sintaxis :
. El siguiente ejemplo ilustra el uso de esta nueva función.
escriba 'una lista
lógica nula: 'lista b
lógica f: 'c lista -> int
objetivo g1: f (nil) = f (nil) (* no válido porque las dos instancias de nil pueden tener
diferentes tipos *)
objetivo g2: f (nulo: 'd lista) = f (nulo:' d lista) (* válido *)
MEDIO AMBIENTE VARIABLES
ERGOLIB
Ruta alternativa para la biblioteca Alt-Ergo
AUTORES
Sylvain Conchón <[email protected]> y Evelyne Contejean <[email protected]>
Use alt-ergo en línea usando los servicios de onworks.net
