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

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

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

4.4.5.3. נאותות ושלמות שיטת Floyd

משפט הנאותות של F – (מערכת ההוכחה של פלויד):

אם מתקיים plot:\[{ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}\]  אז plot:$ \vDash \left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$. במילים: אם ניתן להוכיח את הטענה במערכת ההוכחה Floyd, אז הטענה נכונה.

על מנת להוכיח את המשפט, נציג למת עזר:

למה: אם plot:${ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$ אזי לכל חישוב plot:$\pi $ של P, שמתחיל ממצב plot:${\sigma _0}$ שמקיים: plot:${\sigma _0} \vDash {q_1}\left( {\bar x} \right)$, אם החישוב מגיע לנקודת חתך plot:$l'$ במצב plot:$\sigma '$ אזי plot:$\sigma ' \vDash {I_{l'}}\left( {\bar x} \right)$.

כלומר: אם ניתן במערכת ההוכחה להוכיח את plot:$\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$ אז כל חישוב שמתחיל ממצב plot:${\sigma _0}$ ומספק את תנאי ההתחלה, בהגיעו לנקודת החתך במצב כלשהו, מצב זה מספק את התנאי של נקודת החתך.

הוכחת הלמה תעשה באינדוקציה על מספר נקודות החתך בהן עבר החישוב:

בסיס: חישוב שעבר בנקודת חתך אחת: plot:${l_0} = start,\sigma ' = {\sigma _0},{I_{l'}} = {q_1}$. מתקיים plot:$\sigma ' \vDash {I_{l'}}\left( {\bar x} \right)$ כי נתון שמתקיים plot:${\sigma _0} \vDash {q_1}\left( {\bar x} \right)$.

צעד: ניקח מסלול בו plot:$i + 1$ נקודות חתך. הנחת האינדוקציה היא: plot:${\sigma _i} \vDash {I_{{l_i}}}\left( {\bar x} \right)$ וכן מתקייםplot:${\sigma _i} \vDash {R_{i \to i + 1}}\left( {\bar x} \right)$ (המסלול עביר). צריך להוכיח כי מתקיים: plot:${\sigma _{i + 1}} \vDash {I_{{l_{i + 1}}}}\left( {\bar x} \right)$.

קצת לוגיקה: בעצם מהנתונים מתקיימת טענת הנכונות:

plot:${\sigma _i} \vDash \left( {{I_{{l_i}}}\left( {\bar x} \right) \wedge {R_{i \to i + 1}}\left( {\bar x} \right) = {I_{{l_{1 + 1}}}}\left[ {{T_{{l_i} \to {l_{i + 1}}}}\left( {\bar x} \right)} \right]} \right)$

מטענת הנכונות מתקיים plot:${\sigma _i} \vDash {I_{{l_{1 + 1}}}}\left[ {{T_{{l_i} \to {l_{i + 1}}}}\left( {\bar x} \right)} \right]$. זהו אינו הביטוי המדוייק אותו אנו צריכים להוכיח, לכן נשתמש במשפט מלוגיקה:

תזכורת: מתקיים תמיד plot:$S\left[ {x \leftarrow s\left( e \right)} \right] \vDash \varphi  \Leftrightarrow s \vDash \varphi \left[ {x \leftarrow e} \right]$

  • plot:$S\left[ {x \leftarrow s\left( e \right)} \right]$ זוהי השמה חדשה (אצלנו = מצב חדש) שזהה ל-plot:$s$ חוץ מהערך של plot:$x$ שהוא plot:$s\left( e \right)$, כאשר plot:$\varphi \left[ {x \leftarrow e} \right]$ זו נוסחה בה החלפנו את plot:$x$ בביטוי plot:$e$.


על סמך המשפט בלוגיקה נסיק: plot:${\sigma _i}\left[ {\bar x \leftarrow {T_{{l_{i + 1}}}}\left( {\bar x} \right)} \right] \vDash {I_{{l_{1 + 1}}}}$.

העברנו שינויים בנוסחה לשינויים במצב. מתקיים plot:${\sigma _{i + 1}} \vDash {I_{{l_{i + 1}}}}\left( {\bar x} \right)$ כנדרש.

הוכחת משפט הנאותות:

נניח כי מתקיים plot:${ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$, אזי המצבים האפשריים:

  • אם חישוב plot:$\pi $ של תוכנית אינו עוצר, אז אין דרישה עבורו בנכונות חלקית.
  • חישוב plot:$\pi $ שמתחיל מ-start ממצב plot:$\sigma $ כך ש-plot:$\sigma  \vDash {q_1}\left( {\bar x} \right)$ עוצר. על סמך הלמה ב-halt מתקיימת הטענה plot:${q_2}\left( {\bar x} \right)$.

משפט השלמות עבור F: אם מתקיים plot:$ \vDash \left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$  אז plot:${ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$. כלומר ניתן למצוא נקודות חתך וטענות אינווריאנטיות שמספקות את תנאי הנכונות.

תגיות המסמך:

לפרק הקודם4.4.5.2. דוגמא להפעלת Floyd
לפרק הבא4.4.6. הוכחת עצירה של תוכניות בשפת PLF
אין תגובות!
שיתוף:
| עוד