Đây là lệnh alt-ergo có thể chạy trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks bằng cách sử dụng một trong nhiều máy trạm trực tuyến miễn phí của chúng tôi như Ubuntu Online, Fedora Online, trình giả lập trực tuyến Windows hoặc trình giả lập trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
Alt-Ergo - Một định lý tự động dành riêng cho việc xác minh chương trình
SYNOPSIS
thay thế [ lựa chọn ] hồ sơ
MÔ TẢ
Alt-Ergo là một định lý tự động. Nó có đầu vào là một đa hình tùy ý và
công thức bậc nhất nhiều sắp xếp được viết là một cú pháp tại sao giống như vậy.
LỰA CHỌN
-h Cứu giúp. Sẽ cung cấp cho bạn danh sách đầy đủ các tùy chọn dòng lệnh.
VÍ DỤ
Một lý thuyết về mảng chức năng với các chỉ số nguyên. Lý thuyết này cung cấp một kiểu cài sẵn
('a,' b) farray và một cú pháp tích hợp để thao tác với mảng.
Ví dụ: đã cho một tau kiểu dữ liệu trừu tượng và một mảng chức năng t kiểu (int,
tau) farray được khai báo như sau:
gõ tau
logic t: (int, tau) farray
Các biểu thức:
t [i] biểu thị giá trị được lưu trữ trong t tại chỉ mục i
t [i1 <-v1, ..., in <-vn] biểu thị một mảng lưu trữ các giá trị giống như t cho mọi
chỉ mục ngoại trừ có thể là i1, ..., in, nơi nó lưu trữ giá trị v1, ..., vn. Biểu thức này
tương đương với ((t [i1 <-v1]) [i2 <-v2]) ... [in <-vn].
Các ví dụ.
t [0 <-v] [1 <-w]
t [0 <-v, 1 <-w]
t [0 <-v, 1 <-w] [1]
Một lý thuyết về các kiểu liệt kê.
Ví dụ, kiểu liệt kê t với các hàm tạo A, B, C được định nghĩa như sau
:
loại t = A | B | NS
Có nghĩa là tất cả các giá trị của loại t đều bằng A, B hoặc C. Và tất cả
các hàm tạo này là khác biệt.
Một lý thuyết về các bản ghi đa hình.
Ví dụ, một loại bản ghi đa hình 'tại với hai nhãn a và b thuộc loại' a và
int tương ứng được định nghĩa như sau:
gõ 'at = {a:' a; b: int}
Các biểu thức {a = 4; b = 5} và {r với b = 3} biểu thị các bản ghi, trong khi dấu chấm
ký hiệu ra được sử dụng để truy cập vào các nhãn.
Alt-Ergo (v.> = 0.95) cho phép người dùng buộc loại điều khoản bằng cú pháp :
. Ví dụ dưới đây minh họa việc sử dụng tính năng mới này.
gõ 'một danh sách
logic nil: 'b danh sách
logic f: 'c list -> int
mục tiêu g1: f (nil) = f (nil) (* không hợp lệ vì hai trường hợp nil có thể có
các loại khác nhau *)
mục tiêu g2: f (nil: 'd danh sách) = f (nil:' d danh sách) (* hợp lệ *)
MÔI TRƯỜNG BIẾN
ERGOLIB
Đường dẫn thay thế cho thư viện Alt-Ergo
TÁC GIẢ
Sylvain Conchon <[email được bảo vệ]> và Evelyne Contejean <[email được bảo vệ]>
Sử dụng alt-ergo trực tuyến bằng các dịch vụ onworks.net
