Bu, Ubuntu Online, Fedora Online, Windows çevrimiçi öykünücüsü veya MAC OS çevrimiçi öykünücüsü gibi birden fazla ücretsiz çevrimiçi iş istasyonumuzdan birini kullanarak OnWorks ücretsiz barındırma sağlayıcısında çalıştırılabilen alt-ergo komutudur.
Program:
ADI
Alt-Ergo - Program doğrulamaya adanmış otomatik bir teorem ispatlayıcı
SİNOPSİS
alternatif ergo [ seçenekleri ] dosya
AÇIKLAMA
Alt-Ergo otomatik bir teorem ispatıdır. Girdi olarak keyfi bir polimorfik alır ve
çok sıralı birinci dereceden formül yazılmış bir neden sözdizimidir.
SEÇENEKLER
-h Yardım. Size komut satırı seçeneklerinin tam listesini verecektir.
ÖRNEKLER
Tamsayı indeksli fonksiyonel diziler teorisi. Bu teori yerleşik bir tür sağlar
('a,'b) dizileri işlemek için farray ve yerleşik bir sözdizimi.
Örneğin, soyut bir veri türü tau ve t türünde bir işlevsel dizi (int,
tau) farray şu şekilde ilan edildi:
tau yazın
mantık t : (int, tau) farray
İfadeler:
t[i], i dizininde t'de depolanan değeri belirtir
t[i1<-v1,...,in<-vn], her biri için t ile aynı değerleri depolayan bir diziyi belirtir.
muhtemelen i1,...,in hariç, burada v1,...,vn değerini depolar. Bu ifade
((t[i1<-v1])[i2<-v2])...[in<-vn] ile eşdeğerdir.
Örnekler.
t[0<-v][1<-w]
t[0<-v, 1<-w]
t[0<-v, 1<-w][1]
Bir numaralandırma türleri teorisi.
Örneğin, A, B, C yapıcılarına sahip bir t numaralandırma türü aşağıdaki gibi tanımlanır
:
tip t = A | B | C
Bu, t türünün tüm değerlerinin A, B veya C'ye eşit olduğu anlamına gelir.
bu yapıcılar farklıdır.
Polimorfik kayıtlar teorisi.
Örneğin, 'a ve ' türünde iki etiketli a ve b etiketli 'at' polimorfik bir kayıt türü
int sırasıyla aşağıdaki gibi tanımlanır:
'at = { a : 'a; b : int }
{ a = 4; b = 5 } ve { r with b = 3} kayıtları belirtirken nokta
Etiketlere erişmek için ra notasyonu kullanılır.
Alt-Ergo (v. >= 0.95), kullanıcının sözdizimini kullanarak terimlerin türünü zorlamasını sağlar :
. Aşağıdaki örnek, bu yeni özelliğin kullanımını göstermektedir.
bir liste yazın
mantık sıfır: 'b listesi
mantık f : 'c listesi -> int
gol g1 : f(nil) = f(nil) (* iki nil örneği olabileceği için geçerli değil
farklı şekiller *)
gol g2 : f(nil:'d listesi) = f(nil:'d listesi) (* geçerli *)
ÇEVRE DEĞİŞKENLER
ERGOLİB
Alt-Ergo kitaplığı için alternatif yol
YAZARLAR
Sylvain Conchon <[e-posta korumalı]> ve Evelyne Contejean <[e-posta korumalı]>
onworks.net hizmetlerini kullanarak alt-ergo çevrimiçi kullanın
