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

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

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

4.4.6.2. כלל F* להוכחת עצירה

מטרת כלל זה היא להוכיח plot:$\left\langle {{q_1}} \right\rangle P\left\langle {true} \right\rangle $. דרך הפעולה:

  1. בחרו קבוצה מבוססת היטב plot:$W$ עם סדר חלקי plot:$\left( {W, < } \right)$.
  2. בחרו נקודות חתך (באופן זהה לזה שבחרנו נקודות חתך ב-F).
  3. לכל נקודת חתך, התאימו טענה אינדוקטיבית פרמטרית, plot:$I\left( {\bar x,w} \right)$ כאשר plot:$w$ משתנה שתחומו plot:$W$ ו-plot:$\bar x$ הם משתני התוכנית.
  4. הוכיחו את תנאי הנכונות הבאים:

plot:$\left( {Init} \right)\begin{array}{*{20}{c}}    {} & {}  \\ \end{array} \forall \bar x\left( {{q_1}\left( {\bar x} \right)} \right) \to {\exists _w}{I_{Start}}\left( {\bar x,w} \right)$

עבור כל מסלול plot:$\alpha  = \left( {l,l'} \right)$ ללא נקודות חתך באמצע plot:$\left( {Dec} \right)\begin{array}{*{20}{c}}    {} & {}  \\ \end{array} \forall \bar x\forall w{I_l}\left( {\bar x,w} \right) \wedge {R_\alpha }\left( {\bar x} \right) \to \exists \underbrace {w'}_{ \in W}\left[ {w' < w \wedge {I_{l'}}\left( {{T_a}\left( {\bar x} \right),w'} \right)} \right]$

בצורה כזאת נוכיח plot:$\left\langle {{q_1}} \right\rangle P\left\langle {true} \right\rangle $ - אם תנאי ההתחלה מתקיים, אז התוכנית עוצרת.

באופן אינטואיטיבי לא פורמאלי, נשים לב כי מכיוון שמתקיים שבין כל שתי נקודות חתך  ערכו של plot:$w$ קטן, וכן לא קיימת סדרה יורדת אינסופית ב-plot:$W$, הרי שחייב להיות סוף לתהליך ומכאן התוכנית עוצרת.

אם היינו רוצים גם להוכיח נכונות "באותה הזדמנות" היינו צריכים להוכיח:

plot:$\forall \bar x\forall w{I_{halt}}\left( {\bar x,w} \right) \to {q_2}\left( {\bar x} \right)$ (האינווריאנטה של נקודת העצירה מספקת את תנאי הסיום).

משפט (ללא הוכחה): הכלל F* הוא נאות ושלם.

נאותות F*: אם plot:${ \vdash _{{F^*}}}\left\langle {{q_1}} \right\rangle P\left\langle {true} \right\rangle $ אז plot:$ \vDash \left\langle {{q_1}} \right\rangle P\left\langle {true} \right\rangle $

למה עבור F*: אם plot:${ \vdash _{{F^*}}}\left\langle {{q_1}} \right\rangle P\left\langle {True} \right\rangle $ אזי לכל חישוב plot:$\pi $ של plot:$P$ שמתחיל מ-plot:$Start$ במצב plot:$\sigma $ כך ש-plot:$\sigma  \vDash {q_1}\left( {\bar x} \right)$, אם החישוב מגיע לנקודה plot:$l'$ במצב plot:$\sigma '$ אז קיים plot:$w'$ כך ש-plot:$\sigma ' \vDash {I_{l'}}\left( {\bar x,w'} \right)$.

אינטואציה להוכחת שלמות F*: אם החישוב סופי, נתאים לכל שלב את מספר הצעדים שנשארו עד העצירה.



שאלה לדוגמא

נתונה תוכנית P בשפת תרשימי הזרימה PLF ונתונות טענות plot:${q_1},{q_2}$ מסדר ראשון מעל משתני התוכנית. נאמר ש- plot:$P \vDash {q_1} \to GLOBALLY{q_2}$ אם לכל חישוב של P, אם הוא מתחיל ממצב שמספק את plot:${q_1}$ אז כל מצב על מסלול החישוב מספק את plot:${q_2}$.

הציעו כלל נאות ושלם להוכחת plot:$P \vDash {q_1} \to GLOBALLY{q_2}$. נמקו את נאותות ושלמות הכלל.

פתרון:

  1. בחר את כל צמתי התוכנית כנקודות חתך.
  2. לכל תווית הצמד טענה אינדוקטיבית plot:${I_l}\left( {\bar x} \right)$ כאשר plot:${I_{{l_0}}} = {q_1}\left( {\bar x} \right)$ ו plot:${I_{{l_*}}}\left( {\bar x} \right) = true$
  3. הוכח: plot:$\forall \bar x\left[ {{q_1}\left( {\bar x} \right) \to {q_2}\left( {\bar x} \right)} \right]$
  4. לכל מסלול בסיסי plot:$\tau  = l,l'$ הוכח: plot:$\forall \bar x\left[ {{I_l} \wedge {R_{l,l'}} \wedge {q_2} \to {I_{l'}}\left( {\bar x} \right) \wedge {q_2}\left[ {\bar x \leftarrow {T_{l,l'}}\left( {\bar x} \right)} \right]} \right]$



תגיות המסמך:

לפרק הקודם4.4.6.1. קבוצה מבוססת היטב
לפרק הבא5. לוגיקה של תוכניות
אין תגובות!
שיתוף:
| עוד