Jest to polecenie alt-ergo, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu darmowych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online Windows lub emulator online MAC OS
PROGRAM:
IMIĘ
Alt-Ergo - Automatyczne dowodzenie twierdzeń dedykowane do weryfikacji programu
STRESZCZENIE
alternatywnie [ Opcje ] filet
OPIS
Alt Ergo jest automatycznym dowodzeniem twierdzeń. Jako dane wejściowe przyjmuje dowolny polimorficzny i
napisana wieloskładnikowa formuła pierwszego rzędu jest podobna do składni.
OPCJE
-h Pomoc. Daje pełną listę opcji wiersza poleceń.
PRZYKŁADY
Teoria tablic funkcjonalnych z indeksami całkowitymi. Ta teoria zapewnia wbudowany typ
('a,'b) farray i wbudowaną składnię do manipulowania tablicami.
Na przykład, biorąc pod uwagę abstrakcyjny typ danych tau i tablicę funkcjonalną t typu (int,
tau) farray zadeklarował w następujący sposób:
wpisz tau
logika t : (int, tau) farray
Wyrażenia:
t[i] oznacza wartość przechowywaną w t pod indeksem i
t[i1<-v1,...,in<-vn] oznacza tablicę, która przechowuje te same wartości co t dla każdego
indeks z wyjątkiem prawdopodobnie i1,...,in, gdzie przechowuje wartość v1,...,vn. To wyrażenie
jest równoważne ((t[i1<-v1])[i2<-v2])...[in<-vn].
Przykłady.
t[0<-v][1<-w]
t[0<-v, 1<-w]
t[0<-v, 1<-w][1]
Teoria typów wyliczeniowych.
Na przykład typ wyliczenia t z konstruktorami A, B, C jest zdefiniowany w następujący sposób
:
typ t = A | B | C
Co oznacza, że wszystkie wartości typu t są równe A, B lub C. I to wszystko
te konstruktory są różne.
Teoria zapisów polimorficznych.
Na przykład polimorficzny rekord typu „at z dwiema etykietami a i b typu „a i”
int definiuje się odpowiednio w następujący sposób:
wpisz 'w = { a : 'a; b : wew }
Wyrażenia { a = 4; b = 5 } i { r z b = 3} oznaczają rekordy, natomiast kropka
notacja ra służy do dostępu do etykiet.
Alt-Ergo (v. >= 0.95) pozwala użytkownikowi wymusić typ terminów za pomocą składni :
. Poniższy przykład ilustruje użycie tej nowej funkcji.
wpisz „lista”
logika zero : 'b lista
logika f : 'c lista -> int
cel g1 : f(nil) = f(nil) (* niepoprawne, ponieważ dwa wystąpienia nil mogą mieć
różne rodzaje *)
cel g2 : f(nil:'d lista) = f(nil:'d lista) (* poprawna *)
ŚRODOWISKO ZMIENNE
ERGOLIB
Alternatywna ścieżka do biblioteki Alt-Ergo
AUTORSKI
Sylvaina Conchona <[email chroniony]> i Evelyne Contejean <[email chroniony]>
Korzystaj z alt-ergo online za pomocą usług onworks.net
