Aceasta este comanda alt-ergo care poate fi rulată în furnizorul de găzduire gratuit OnWorks folosind una dintre multiplele noastre stații de lucru online gratuite, cum ar fi Ubuntu Online, Fedora Online, emulator online Windows sau emulator online MAC OS
PROGRAM:
NUME
Alt-Ergo - Un demonstrator automat de teoreme dedicat verificării programelor
REZUMAT
alt-ergo [ Opțiuni ] fişier
DESCRIERE
Alt-Ergo este un demonstrator automat de teoreme. Ia ca intrări un polimorf și arbitrar
formula multi-sortată de ordinul întâi scrisă este o sintaxă asemănătoare motivului.
OPŢIUNI
-h Ajutor. Vă va oferi lista completă de opțiuni pentru linia de comandă.
EXEMPLE
O teorie a tablourilor funcționale cu indici întregi. Această teorie oferă un tip încorporat
('a,'b) farray și o sintaxă încorporată pentru manipularea tablourilor.
De exemplu, având în vedere un tip de date abstract tau și o matrice funcțională de tip t (int,
tau) Farray a declarat după cum urmează:
tip tau
logic t : (int, tau) farray
Expresiile:
t[i] denotă valoarea stocată în t la indicele i
t[i1<-v1,...,in<-vn] denotă o matrice care stochează aceleași valori ca t pentru fiecare
index, cu excepția eventualului i1,...,in, unde stochează valoarea v1,...,vn. Această expresie
este echivalent cu ((t[i1<-v1])[i2<-v2])...[in<-vn].
Exemple.
t[0<-v][1<-w]
t[0<-v, 1<-w]
t[0<-v, 1<-w][1]
O teorie a tipurilor de enumerare.
De exemplu, o enumerare de tip t cu constructori A, B, C este definită după cum urmează
:
tip t = A | B | C
Ceea ce înseamnă că toate valorile de tip t sunt egale fie cu A, B sau C. Și toate acestea
acești constructori sunt diferiți.
O teorie a înregistrărilor polimorfe.
De exemplu, o înregistrare polimorfă de tip 'at cu două etichete a şi b de tip 'a şi
int este definit după cum urmează:
tip 'at = { a : 'a; b : int }
Expresiile { a = 4; b = 5 } și { r cu b = 3} denotă înregistrări, în timp ce punctul
notația ra este folosită pentru a accesa etichete.
Alt-Ergo (v. >= 0.95) permite utilizatorului să forțeze tipul de termeni folosind sintaxa :
. Exemplul de mai jos ilustrează utilizarea acestei noi caracteristici.
tastați „o listă”.
logic nil : 'b listă
logic f : 'c list -> int
obiectivul g1 : f(nil) = f(nil) (* nu este valabil deoarece cele două cazuri de zero pot avea
tipuri diferite *)
obiectiv g2 : f(nil:'d list) = f(nil:'d list) (* valid *)
MEDIUL VARIABILE
ERGOLIB
Cale alternativă pentru biblioteca Alt-Ergo
AUTORI
Sylvain Conchon <[e-mail protejat]> și Evelyne Contejean <[e-mail protejat]>
Utilizați alt-ergo online folosind serviciile onworks.net
