นี่คือคำสั่ง cafeobj ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
cafeobj - ข้อกำหนดเกี่ยวกับพีชคณิตและภาษาการเขียนโปรแกรม
เรื่องย่อ
คาเฟ่ออบเจ [ทางเลือกที่-ไฟล์] ...
DESCRIPTION
เริ่ม คาเฟ่OBJ ล่าม.
คาเฟ่OBJ เป็นภาษาข้อกำหนดที่เป็นทางการขั้นสูงที่สุดซึ่งสืบทอดขั้นสูงมากมาย
คุณสมบัติ (เช่น ไวยากรณ์ผสมแก้ไขที่ยืดหยุ่น ระบบการพิมพ์ที่ทรงพลังและชัดเจนพร้อมคำสั่ง
การเรียงลำดับ โมดูลพารามิเตอร์และมุมมองสำหรับการสร้างอินสแตนซ์ของพารามิเตอร์ และโมดูล
นิพจน์ ฯลฯ) จากภาษาข้อกำหนดเกี่ยวกับพีชคณิต OBJ (หรือมากกว่า OBJ3)
CafeOBJ เป็นภาษาสำหรับการเขียนข้อกำหนดทางการ (เช่น คณิตศาสตร์) ของแบบจำลองสำหรับ
ซอฟต์แวร์และระบบที่หลากหลาย และการตรวจสอบคุณสมบัติของซอฟต์แวร์เหล่านั้น คาเฟ่OBJ
ใช้ตรรกะสมการโดยการเขียนใหม่และสามารถใช้เป็นทฤษฎีบทเชิงโต้ตอบที่ทรงพลังได้
ระบบการพิสูจน์ Specifiers สามารถเขียนคะแนนการพิสูจน์ได้ใน CafeOBJ และทำการพิสูจน์ด้วย
ดำเนินการคะแนนการพิสูจน์
CafeOBJ มีความหมายเชิงตรรกะที่เข้มงวดล้ำสมัยตามสถาบันต่างๆ The CafeOBJ
ลูกบาศก์แสดงโครงสร้างของตรรกะต่างๆ
กระบวนทัศน์ที่ดำเนินการโดยภาษา คะแนนการพิสูจน์ใน CafeOBJ ก็ขึ้นอยู่กับ
ความหมายที่เข้มงวดตามสถาบันและสามารถสร้างได้โดยใช้ชุดการพิสูจน์ที่สมบูรณ์
กฎระเบียบ
OPTIONS
มีตัวเลือกสองคลาส อย่างแรกคือตัวเลือกสำหรับ คาเฟ่ออบเจ สคริปต์ wrapper
ที่อนุญาตให้เลือกล่าม Common Lisp พื้นฐานและปรับเส้นทางการค้นหา
พารามิเตอร์
- เครื่องยนต์ ชื่อ
เลือกเอ็นจิ้นเสียงกระเพื่อมทั่วไปพื้นฐาน ถ้าไม่ให้ เลือกอันแรก
ระหว่างเวลาที่ใช้สร้าง
-รายการเครื่องยนต์
แสดงรายการเครื่องยนต์ Lisp ทั่วไปที่มีอยู่ทั้งหมด
-wrapper-libpath เส้นทาง
กำหนดเส้นทางที่จะพบการทิ้งหน่วยความจำของตัวแปลเสียงกระเพื่อม
-wrapper-sharepath เส้นทาง
กำหนดเส้นทางที่จะค้นหาไฟล์เริ่มต้นของ CafeOBJ
ชุดตัวเลือกต่อไปนี้ส่งไปที่ล่ามของ CafeOBJ โดยตรง:
-ช่วยด้วย พิมพ์ข้อความช่วยเหลือ
-q อย่าโหลดไฟล์เริ่มต้นของผู้ใช้
-แบทช์ ทำงานในโหมดแบตช์
-p เส้นทาง
ให้โมดูลการกำหนดไฟล์โหมโรงมาตรฐาน
+p เส้นทาง
โหลดไฟล์โหมโรงเพิ่มเติม
-l DIR-รายการ
ตั้งค่ารายชื่อพาธสำหรับพาธการค้นหาโมดูล คั่นด้วยเครื่องหมายทวิภาค
+l DIR-รายการ
เพิ่มรายการชื่อเส้นทางสำหรับเส้นทางการค้นหาโมดูล
ไฟล์ ไฟล์ที่โหลดในเวลาเริ่มต้นตามลำดับ
ใช้ cafeobj ออนไลน์โดยใช้บริการ onworks.net