Đây là lệnh cafeobj 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 mô phỏng trực tuyến Windows hoặc trình mô phỏng trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
cafeobj - ngôn ngữ lập trình và đặc tả đại số
SYNOPSIS
cafeobj [TÙY CHỌN] ... [CÁC TẬP TIN] ...
MÔ TẢ
Bắt đầu CafeOBJ thông dịch viên.
CafeOBJ là ngôn ngữ đặc tả hình thức tiên tiến nhất kế thừa nhiều ngôn ngữ tiên tiến
các tính năng (ví dụ: cú pháp sửa lỗi linh hoạt, hệ thống gõ mạnh mẽ và rõ ràng với thứ tự
sắp xếp, mô-đun tham số và chế độ xem để khởi tạo các tham số và mô-đun
biểu thức, v.v.) từ ngôn ngữ đặc tả đại số OBJ (hay chính xác hơn là OBJ3).
CafeOBJ là ngôn ngữ để viết các đặc tả hình thức (tức là toán học) của các mô hình cho
nhiều loại phần mềm và hệ thống cũng như xác minh các thuộc tính của chúng. CafeOBJ
thực hiện logic phương trình bằng cách viết lại và có thể được sử dụng như một định lý tương tác mạnh mẽ
hệ thống chứng minh. Người xác định cũng có thể viết điểm chứng minh trong CafeOBJ và thực hiện chứng minh bằng cách
thực hiện việc chấm điểm chứng minh.
CafeOBJ có ngữ nghĩa logic nghiêm ngặt hiện đại dựa trên các tổ chức. Quán cà phêOBJ
khối lập phương cho thấy cấu trúc của các logic khác nhau làm cơ sở cho sự kết hợp của các logic khác nhau
các mô hình được thực hiện bởi ngôn ngữ. Điểm chứng minh trong CafeOBJ cũng dựa trên
ngữ nghĩa chặt chẽ dựa trên tổ chức và có thể được xây dựng bằng cách sử dụng một bộ bằng chứng hoàn chỉnh
quy tắc.
LỰA CHỌN
Có hai loại tùy chọn. Đầu tiên là các tùy chọn cho cafeobj kịch bản bao bọc
cho phép chọn trình thông dịch Common Lisp cơ bản và điều chỉnh đường dẫn tìm kiếm
thông số.
-động cơ TÊN
chọn công cụ lisp chung cơ bản. Nếu không được đưa ra, cái đầu tiên được chọn
trong thời gian xây dựng được sử dụng.
-list-động cơ
liệt kê tất cả các công cụ lisp phổ biến có sẵn
-wrapper-libpath PATH
đặt đường dẫn nơi tìm thấy vùng lưu trữ bộ nhớ của trình thông dịch lisp
-wrapper-sharepath PATH
đặt đường dẫn tìm kiếm các tệp khởi tạo CafeOBJ
Bộ tùy chọn sau đây được hướng trực tiếp đến trình thông dịch CafeOBJ:
-Cứu giúp in một tin nhắn trợ giúp
-q không tải tập tin khởi tạo của người dùng
-lô hàng chạy ở chế độ hàng loạt
-p PATH
cung cấp các mô-đun xác định tập tin mở đầu tiêu chuẩn
+p PATH
tải tập tin dạo đầu bổ sung
-l DANH SÁCH TRỰC TIẾP
đặt danh sách tên đường dẫn cho đường dẫn tìm kiếm mô-đun, phân tách bằng dấu hai chấm
+l DANH SÁCH TRỰC TIẾP
thêm danh sách tên đường dẫn cho đường dẫn tìm kiếm mô-đun
CÁC TẬP TIN các tập tin được tải vào lúc khởi động theo thứ tự.
Sử dụng cafeobj trực tuyến bằng dịch vụ onworks.net
