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

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

4.4.5. כלל ההוכחה F ( (Floyd לתוכניות תרשים זרימה עם חוגים

כלל ההוכחה של Floyd משמש אותנו להוכחת $plot:$\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$$ . נשתמש בכלל הבא:

א. נקודת ההתחלה $plot:${l_0}$$ $plot:$\left( {start} \right)$$ תהיה נקודת חתך.

ב. נקודת הסיום $plot:${l_{halt}}$$ $plot:$\left( {halt} \right)$$ תהיה נקודת חתך.

ג. כל מעגל בגרף התוכנית יכיל לפחות נקודת חתך אחת.

לכל נקודת חתך , נמצא טענה אינדוקטיבית (invariant שמורה) $plot:\[{I_l}\left( {\bar x} \right)\]$ . כמו כן, תמיד נבחר: $plot:${I_{start}}\left( {\bar x} \right) = {q_1}\left( {\bar x} \right)$$ , $plot:${I_{halt}}\left( {\bar x} \right) = {q_2}\left( {\bar x} \right)$$ .
לכל מסלול $plot:$\alpha = \left( {{l_i},{l_j}} \right)$$ שלא עובר דרך נקודות חתך אחרות נוכיח את תנאי הנכונות: $plot:${I_l}_i\left( {\bar x} \right) \wedge {R_\alpha }\left( {\bar x} \right) \to {I_l}_j\left[ {\bar x \leftarrow {T_\alpha }\left( {\bar x} \right)} \right]$$ .

(אם מתקיים התנאי הראשון על המשתנים בנקודה הראשונה וגם המסלול עביר אז יתקיים התנאי השני על הטרנספורמר של המסלול על המשתנים).

אם הפעלנו את הכלל בהצלחה נסמן: $plot:\[{ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}\]$

הערות:

כאשר מדובר על תוכנית עם מעגלים נכונות חלקית ונכונות מלאה לא מתלכדים. כלל Floyd מוכיח נכונות חלקית בלבד.
הרעיון מאחורי בחירת נקודות החתך הוא לדאוג שכל מסלול בין 2 נקודות חתך יהיה סופי.