הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

4.4.4. כלל להוכחת נכונות עבור תוכניות ללא מעגלים

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

תוכנית ללא מעגלים P נכונה ביחס למפרט plot:$ < {q_1},{q_2} > $ (כלומר plot:$ < {q_1} > P < {q_2} > $) אם ורק אם לכל מסלול מלא plot:$\tau $ של P מתקיים:  plot:${q_1}\left( {\bar x} \right) \wedge {R_\tau }\left( {\bar x} \right) \to {q_2}\left( {{T_\tau }\left( {\bar x} \right)} \right)$. (אם תנאי ההתחלה מתקיים והמסלול עביר אז תנאי הסיום מתקיים על הטרנספורמר של משתני ההתחלה).

אופן הפעולה:

  1. לכל מסלול מ-start ל-halt נחשב plot:${T_\tau }\left( {\bar x} \right)$ ו-plot:${R_\tau }\left( {\bar x} \right)$.
  2. לכל מסלול כנ"ל נוכיח: plot:$\forall \bar x\left[ {{q_1}\left( {\bar x} \right) \wedge {R_\tau }\left( {\bar x} \right) \to {q_2}\left( {{T_\tau }\left( {\bar x} \right)} \right)} \right]$

תגיות המסמך:

לפרק הקודם4.4.3. הגדרה אינדוקטיבית של plot:${T_\tau }\left( {\bar x} \right)$ ושל plot:${R_\tau }\left( {\bar x} \right)$
לפרק הבא4.4.5. כלל ההוכחה F ( (Floyd לתוכניות תרשים זרימה עם חוגים
אין תגובות!
שיתוף:
| עוד