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

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

5.1.4.1. אקסיומות

אקסיומת ההצבה - $plot:$\left\{ {p\left[ {x \leftarrow e} \right]} \right\}x: = e\left\{ p \right\}$$ . (תסומן ב-ASS)

האקסיומה הראשונה שנציג הינה אקסיומת ההצבה. אקסיומה זו מעט מסובכת להבנה בהתקלות ראשונה, ולכן נסביר אותה בפירוט. דגש ראשון: את אקסיומת ההצבה קוראים מימין לשמאל.

$plot:$p\left[ {x \leftarrow e} \right]$$ הוא התנאי החלש ביותר שמבטיח ש- plot:$p$ יתקיים לאחר ביצוע plot:$x: = e$ . משמעותו: לקחנו את התוכנית והצבנו בכל מקום במקום plot:$x$ את הערך plot:$e$ .

דוגמא 1: נביט בחלק הימני: $plot:$x: = x + 5\left\{ {x < 0} \right\}$$ - השאלה שאנחנו שואלים הינה: "מה צריך לדרוש כדי שיתקיים plot:$x < 0$ אחרי ביצוע של הפעולה plot:$x:
= x + 5$ ?". התשובה היא plot:$x < -
5$ , ולכן נכתוב: $plot:$\left\{ {x < - 5} \right\}x: = x + 5\left\{ {x < 0} \right\}$$ . מבחינת טכניקה: נוכל לקבל את הצד השמאלי על ידי הצבת plot:$e$ בכל מקום שבו מופיע plot:$x$ ב- plot:$p$ , וכך לייצר את הצד השמאלי.

לחילופין, אם נתון רק הצד השמאלי: $plot:$\left\{ p \right\}y: = t\left\{ ? \right\}$$ אנחנו יכולים ליצור את הצד הימני באופן אינטואיטיבי, על ידי הפעלת הפקודה שבתוכנית על החלק השמאלי.

ניסוח חלופי לאקסיומת ההצבה: מדוע לא ניסחנו טענה בסגנון $plot:$\left\{ {true} \right\}x: = e\left\{ {x = e} \right\}$$ ? מכיוון שכאן אין קשר בין המצב ההתחלתי לסופי. ראו לדוגמא: $plot:$\left\{ {true} \right\}x: = x + 1\left\{ {\underbrace {x = x + 1}_{false}} \right\}$$ . כאשר plot:$e$ אינו תלוי ב- plot:$x$ מתקיים כי $plot:$\left\{ {true} \right\}x: = e\left\{ {x = e} \right\}$$ היא אקסיומה נכונה. למשל: $plot:$\left\{ {true} \right\}x: = 5\left\{ {x = 5} \right\}$$