cafeobj - מקוון בענן

תָכְנִית:

שֵׁם

cafeobj - מפרט אלגברי ושפת תכנות

תַקצִיר

cafeobj [אוֹפְּצִיָה]... [קבצים] ...

תיאור

מתחיל את CafeOBJ מְתוּרגְמָן.

CafeOBJ היא שפת מפרט פורמלי מתקדמת ביותר שיורשת מתקדמים רבים
תכונות (למשל תחביר גמיש ל-mix-fix, מערכת הקלדה חזקה וברורה עם הזמנה
מיון, מודולים פרמטריים ותצוגות לאינסטציה של הפרמטרים, ומודול
ביטויים וכו') משפת המפרט האלגברי של OBJ (או ליתר דיוק OBJ3).

CafeOBJ היא שפה לכתיבת מפרטים פורמליים (כלומר מתמטיים) של מודלים עבור
מגוון רחב של תוכנות ומערכות, ואימות המאפיינים שלהן. CafeOBJ
מיישמת לוגיקה משוואה על ידי כתיבה מחדש ויכולה לשמש כמשפט אינטראקטיבי רב עוצמה
מערכת הוכחה. מפרטים יכולים לכתוב ציוני הוכחה גם ב- CafeOBJ ולבצע הוכחות על ידי
ביצוע ציוני ההוכחה.

ל- CafeOBJ יש סמנטיקה לוגית קפדנית מתקדמת המבוססת על מוסדות. בית הקפה OBJ
קובייה מציגה את מבנה ההגיונות השונים העומדים בבסיס השילוב של השונות
פרדיגמות המיושמות על ידי השפה. ציוני ההוכחה ב-CafeOBJ מבוססים גם על
סמנטיקה קפדנית המבוססת על מוסד, וניתן לבנות אותה באמצעות סט שלם של הוכחות
כללים.

אפשרויות

יש שני סוגים של אפשרויות. הראשונה הן אפשרויות עבור cafeobj סקריפט עטיפה
המאפשר לבחור את המתורגמן הבסיסי של Common Lisp, ולהתאים את נתיב החיפוש
פרמטרים.

-מנוע שֵׁם
בוחר את מנוע ה-lisp המשותף הבסיסי. אם לא ניתן, נבחר הראשון
בזמן הבנייה נעשה שימוש.

-מנועי רשימת
מפרט את כל מנועי lisp הנפוצים הזמינים

-עטיפה-libpath נתיב
מגדיר את הנתיב שבו נמצאות מזימות זיכרון של מתורגמני lisp

-עטיפה-שיתוף נתיב נתיב
מגדיר את הנתיב שבו מחפשים קבצי אתחול CafeOBJ

קבוצת האפשרויות הבאה מכוונת ישירות למתורגמן CafeOBJ:

עזרה להדפיס הודעת עזרה

-q אל תטען את קובץ האתחול של המשתמש

-קבוצה להפעיל במצב אצווה

-p נתיב
נותן את מודולי ההגדרה של קובץ ההקדמה הסטנדרטי

+p נתיב
טען קובץ הקדמה נוסף

-l רשימת מנהלים
הגדר רשימה של שמות נתיבים עבור נתיב חיפוש מודול, מופרד על ידי נקודתיים

+l רשימת מנהלים
מוסיף רשימה של שם נתיב עבור נתיב חיפוש מודול

קבצים קבצים שנטענים בזמן ההפעלה לפי הסדר.

השתמש ב-cafeobj באינטרנט באמצעות שירותי onworks.net