alt-ergo - מקוון בענן

תָכְנִית:

שֵׁם

Alt-Ergo - מוכיח משפט אוטומטי המוקדש לאימות תוכניות

תַקצִיר

אל-ארגו [ אפשרויות ] פילה

תיאור

אלט-ארגו הוא מוכיח משפט אוטומטי. זה לוקח כקלט פולימורפי ו שרירותי
נוסחה מרובה מיון שנכתבה מסדר ראשון היא תחביר כמו למה.

אפשרויות

-h עֶזרָה. ייתן לך את הרשימה המלאה של אפשרויות שורת הפקודה.

דוגמאות

תיאוריה של מערכים פונקציונליים עם אינדקסים שלמים. תיאוריה זו מספקת סוג מובנה
('a,'b) farray ותחביר מובנה למניפולציה של מערכים.

לדוגמה, בהינתן סוג נתונים מופשט tau ומערך פונקציונלי t של סוג (int,
tau) farray הכריז כדלקמן:

סוג טאו

logic t : (int, tau) farray

הביטויים:

t[i] מציין את הערך המאוחסן ב-t באינדקס i

t[i1<-v1,...,in<-vn] מציין מערך שמאחסן את אותם ערכים כמו t עבור כל
אינדקס למעט אולי i1,...,in, שבו הוא מאחסן ערך v1,...,vn. הביטוי הזה
שווה ל-((t[i1<-v1])[i2<-v2])...[in<-vn].

דוגמאות.

t[0<-v][1<-w]

t[0<-v, 1<-w]

t[0<-v, 1<-w][1]

תיאוריה של סוגי ספירה.

לדוגמה, סוג ספירה t עם בנאים A, B, C מוגדר כדלקמן
:

הקלד t = A | ב | ג

מה שאומר שכל הערכים מסוג t שווים ל-A, B או C. וזה הכל
הבנאים הללו הם שונים.

תיאוריה של רשומות פולימורפיות.

לדוגמה, סוג רשומה פולימורפי 'at עם שתי תוויות a ו-b מסוג 'a ו
int בהתאמה מוגדר כדלקמן:

הקלד 'at = { a : 'a; b : int }

הביטויים { a = 4; b = 5 } ו- { r עם b = 3} מציינים רשומות, בעוד הנקודה
סימון ra משמש לגישה לתוויות.

Alt-Ergo (v. >= 0.95) מאפשר למשתמש לאלץ את סוג המונחים באמצעות התחביר :
. הדוגמה להלן ממחישה את השימוש בתכונה חדשה זו.

הקלד 'רשימה'

היגיון אפס: 'ב רשימה

logic f : 'c list -> int

יעד g1 : f(nil) = f(nil) (* לא תקף כי ייתכן ששני המקרים של nil
סוגים שונים *)

goal g2 : f(nil:'d list) = f(nil:'d list) (* חוקי *)

הסביבה וריאציות

ארגוליב
נתיב חלופי לספריית Alt-Ergo

מחברים

סילבן קונצ'ון <conchon@lri.fr> ואוולין קונטז'אן <contejea@lri.fr>

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