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

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

4.4.5.2. דוגמא להפעלת Floyd

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

הפעלת Floyd:

נגדיר את $plot:${q_1}\left( {\bar x} \right)$$ ואת $plot:${q_2}\left( {\bar x} \right)$$ :

כל ערכי המשתנים בתוכנית הינם מעל $plot:$\mathbb{Z}$$ .
$plot:${q_1}\left( {{x_1},{x_2},q,r,{X_1},{X_2}} \right) = \left( {{x_1} = {X_1} \wedge {x_2} = {X_2} \wedge {x_1} \geqslant 0 \wedge {x_2} > 0} \right)$$
$plot:${q_2}\left( {{x_1},{x_2},q,r,{X_1},{X_2}} \right) = \left( {{X_1} = q{X_2} + r \wedge 0 \leqslant r < {X_2}} \right)$$

נבחר טענות עבור נקודות החתך:

נצמיד לצומת $plot:${l_0}$$ את הטענה $plot:${q_1}\left( {\bar x} \right)$$ ונצמיד ל- $plot:${l_*}$$ את הטענה $plot:${q_2}\left( {\bar x} \right)$$ .
נציע טענה: $plot:${I_{{l_4}}} = \left( {{X_1} = q{X_2} + r \wedge r \geqslant 0 \wedge {x_1} = {X_1} \wedge {x_2} = {X_2}} \right)$$ . אם האינוריאנטה מתקיימת ובחרנו לצאת מהלולאה, הרי שהטענה תבטיח את $plot:${q_2}$$ בסיום, ולכן זו נראית טענה מוצלחת.

צריך להוכיח את תנאי הנכונות לכל המסלולים הסופיים. המסלולים הקיימים: $plot:${l_0}{l_4},\,\,{l_4}{l_4},\,\,{l_4}{l_5}$$ .

נראה את תנאי הנכונות עבור $plot:${l_4}{l_4}$$ .

צ"ל: $plot:${I_l}_{_4}\left( {\bar x} \right) \wedge {R_{{l_4}{l_4}}}\left( {\bar x} \right) \to {I_{{l_4}}}\left[ {\bar x \leftarrow {T_{{l_4}{l_4}}}\left( {\bar x} \right)} \right]$$

$plot:$\begin{gathered} {R_{{l_4}{l_4}}}\left( {\bar x} \right) = \left( {r \geqslant {x_2}} \right) \hfill \\ {T_{{l_4}{l_4}}}\left( {{x_1},{x_2},q,r,{X_1},{X_2}} \right) = \left( {{x_1},{x_2},q + 1,r - {x_2},{X_1},{X_2}} \right) \hfill \\ \end{gathered} $$

נציב בתנאי:

$plot:\[\begin{gathered} \left( {{X_1} = q{X_2} + r \wedge r \geqslant 0 \wedge {x_1} = {X_1} \wedge {x_2} = {X_2}} \right) \wedge \left( {r \geqslant {x_2}} \right) \to \hfill \\ \left( {{X_1} = \left( {q + 1} \right){X_2} + \left( {r - {X_2}} \right) \wedge r - {X_2} \geqslant 0 \wedge {x_1} = {X_1} \wedge {x_2} = {X_2}} \right) \hfill \\ \end{gathered} \]$

קיבלנו נוסחה בלוגיקה. לצורך הוכחת אימות תוכנה מספיק לנו לראות שהנוסחה

נכונה מבחינה מתמטית – אין צורך להכנס להוכחה מורכבת בלוגיקה. ממתמטיקה

טריויאלית ניתן לראות את נכונות הביטוי.

תנאי נכונות עבור $plot:${l_0}{l_4}$$ ו- $plot:${l_4}{l_5}$$ יחושבו בצורה דומה.
אחרי ההוכחות נאמר כי $plot:\[{ \vdash _F}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}\]$ .