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

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

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

4.4.3. הגדרה אינדוקטיבית של plot:${T_\tau }\left( {\bar x} \right)$ ושל plot:${R_\tau }\left( {\bar x} \right)$

יהי מסלול plot:$\tau  = \left( {{l_{i0}},...,{l_{ik}}} \right)$. נחשב סדרה של ביטויים plot:$T_\tau ^j\left( {\bar x} \right),R_\tau ^j\left( {\bar x} \right)$ על המסלול מהסוף להתחלה, כלומר נתחיל ב-plot:$j = k$ ונסיים ב-plot:$j = 0$.

  • plot:$T_\tau ^j\left( {\bar x} \right)$ מציין את טרנספורמצית המצבים על המסלול plot:$\left( {{l_{ij}},...,{l_{ik}}} \right)$
  • plot:$R_\tau ^j\left( {\bar x} \right)$ הינו תנאי הישיבות המסלול plot:$\left( {{l_{ij}},...,{l_{ik}}} \right)$

הערה: צריך לשים לב שכאשר אנחנו מסתכלים על חישוב מסלול, החישוב plot:$\left( {{l_{ij}},...,{l_{ik}}} \right)$ אינו כולל את ביצוע הפקודה הרשומה ב-plot:${l_{ik}}$.

בסיס ההגדרה: plot:$T_\tau ^k\left( {\bar x} \right) = \left( {\bar x} \right)$,          plot:$R_\tau ^k\left( {\bar x} \right) = true$

            הסבר: בשלב זה המסלול הוא plot:${l_{ik}}$ ולכן:

  • המשתנים בסיום זהים למשתנים בהתחלה.
  • התנאי למעבר הוא plot:$true$.

צעד האינדוקציה: בהינתן plot:$T_\tau ^{k + 1}$, plot:$R_\tau ^{k + 1}$ נרצה לחשב  plot:$T_\tau ^k$, plot:$R_\tau ^k$.

א. הצבה: plot:$\bar x: = \bar e$  :              plot:$\begin{gathered}   R_\tau ^k\left( {\bar x} \right) = R_\tau ^{k + 1}\left[ {\bar x \leftarrow \bar e} \right] \hfill \\   T_\tau ^k\left( {\bar x} \right) = T_\tau ^{k + 1}\left[ {\bar x \leftarrow \bar e} \right] \hfill \\ \end{gathered} $

ב. תנאי :  plot:$b\left( {\bar x} \right)$  : אם זה הצד החיובי של התנאי: plot:$\begin{gathered}   R_\tau ^k\left( {\bar x} \right) = R_\tau ^{k + 1}\left( {\bar x} \right) \wedge b\left( {\bar x} \right) \hfill \\   T_\tau ^k\left( {\bar x} \right) = T_\tau ^{k + 1}\left( {\bar x} \right) \hfill \\ \end{gathered} $

                            אם זה הצד השלילי של התנאי: plot:$\begin{gathered}   R_\tau ^k\left( {\bar x} \right) = R_\tau ^{k + 1}\left( {\bar x} \right) \wedge \neg b\left( {\bar x} \right) \hfill \\   T_\tau ^k\left( {\bar x} \right) = T_\tau ^{k + 1}\left( {\bar x} \right) \hfill \\ \end{gathered} $

אופן החישוב: נחשב את plot:${T_\tau }\left( {\bar x} \right)$ ואת plot:${R_\tau }\left( {\bar x} \right)$ ע"י חישוב "אחורנית": בהינתן מסלול plot:$\tau  = {l_{i0}},{l_{i1}},...,{l_{ik}}$ נתחיל עם plot:\[T_\tau ^k\left( {\bar x} \right)\] ונסיים עם plot:\[T_\tau ^0\left( {\bar x} \right)\]. יתקיים: plot:\[{T_\tau }\left( {\bar x} \right) = T_\tau ^0\left( {\bar x} \right)\].



דוגמא: יהא תרשים הזרימה הבא:

הביטו כעת בטבלה. שימו לב כשאתם קוראים את הטבלה הבאה שבנייתה החלה מ-plot:${l_4}$ ונמשכה כלפי מעלה אל הצמתים הראשונות. באפור – המסקנות אליהן אנו מגיעים.

plot:$\tau  = {l_0},{l_1},{l_3},{l_4}$ מסלול ימני

plot:$\tau  = {l_0},{l_1},{l_2},{l_4}$ מסלול שמאלי

plot:$T_\tau ^0\left( {\bar x} \right) = \left( {x, - x} \right)$          plot:${l_0}:start$

plot:$T_\tau ^1\left( {\bar x} \right) = \left( {x, - x} \right)$          plot:${l_1}:x > 0$

plot:$T_\tau ^2\left( {\bar x} \right) = \left( {x, - x} \right)$          plot:${l_3}:y: =  - x$

plot:$T_\tau ^3\left( {\bar x} \right) = \left( {x,y} \right)$          plot:${l_4}:halt$

plot:$T_\tau ^0\left( {\bar x} \right) = \left( {x,x} \right)$          plot:${l_0}:start$

plot:$T_\tau ^1\left( {\bar x} \right) = \left( {x,x} \right)$          plot:${l_1}:x > 0$

plot:$T_\tau ^2\left( {\bar x} \right) = \left( {x,x} \right)$          plot:${l_2}:y: = x$

plot:$T_\tau ^3\left( {\bar x} \right) = \left( {x,y} \right)$          plot:${l_4}:halt$

plot:${T_\tau }\left( {\bar x} \right) = T_\tau ^0\left( {\bar x} \right) = \left( {x, - x} \right)$

plot:${T_\tau }\left( {\bar x} \right) = T_\tau ^0\left( {\bar x} \right) = \left( {x,x} \right)$

plot:$R_\tau ^0\left( {x,y} \right) = x \leqslant 0$          plot:${l_0}:start$

plot:$R_\tau ^1\left( {x,y} \right) = x \leqslant 0$          plot:${l_1}:x > 0$

plot:$R_\tau ^2\left( {x,y} \right) = True\left[ {y \leftarrow  - x} \right] = True$    plot:${l_3}:y: =  - x$

plot:$R_\tau ^3\left( {x,y} \right) = True$          plot:${l_4}:halt$

plot:$R_\tau ^0\left( {x,y} \right) = x > 0$          plot:${l_0}:start$

plot:$R_\tau ^1\left( {x,y} \right) = x > 0$          plot:${l_1}:x > 0$

plot:$R_\tau ^2\left( {x,y} \right) = True\left[ {y \leftarrow x} \right] = True$  plot:${l_2}:y: = x$

plot:$R_\tau ^3\left( {x,y} \right) = True$          plot:${l_4}:halt$

plot:${R_\tau }\left( {\bar x} \right) = R_\tau ^0\left( {x,y} \right) = x \leqslant 0$

plot:${R_\tau }\left( {\bar x} \right) = R_\tau ^0\left( {x,y} \right) = x > 0$



תגיות המסמך:

לפרק הקודם4.4.2. דוגמאות לעבירות
לפרק הבא4.4.4. כלל להוכחת נכונות עבור תוכניות ללא מעגלים
אין תגובות!
שיתוף:
| עוד