4.4.5. כלל ההוכחה F ( (Floyd לתוכניות תרשים זרימה עם חוגים
כלל ההוכחה של Floyd משמש אותנו להוכחת
. נשתמש בכלל הבא:
- נבחר "נקודות חתך" בתוכנית בצורה הבאה:
א.
נקודת ההתחלה
תהיה נקודת חתך.
ב.
נקודת הסיום
תהיה נקודת חתך.
ג.
כל מעגל בגרף התוכנית יכיל לפחות נקודת חתך אחת.
- לכל נקודת חתך
, נמצא טענה אינדוקטיבית (invariant
שמורה)
. כמו כן, תמיד נבחר:
,
.
- לכל מסלול
שלא עובר דרך נקודות חתך
אחרות נוכיח את תנאי הנכונות:
.
(אם מתקיים התנאי הראשון על המשתנים בנקודה הראשונה וגם המסלול עביר אז
יתקיים התנאי השני על הטרנספורמר של המסלול על המשתנים).
אם הפעלנו את הכלל בהצלחה נסמן: ![plot:\[{ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}\]](/documentResources/326/plot_184.png)
הערות:
- כאשר מדובר על
תוכנית עם מעגלים נכונות חלקית ונכונות מלאה לא מתלכדים. כלל Floyd
מוכיח נכונות חלקית בלבד.
- הרעיון מאחורי
בחירת נקודות החתך הוא לדאוג שכל מסלול בין 2 נקודות חתך יהיה סופי.