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

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

5.1.4.3. משפט הנאותות של H

משפט: אם $plot:${ \vdash _h}\left\{ p \right\}S\left\{ q \right\}$$ אז $plot:$ \vDash \left\{ p \right\}S\left\{ q \right\}$$

ההוכחה תהיה באינדוקציה על מבנה ההוכחה ב-H. נראה שכל אחת מהאקסיומות תמיד נכונה. נראה כי לכל כלל היסק, אם מתקיים החלק העליון שבכלל, אזי מתקיים גם החלק התחתון.

בסיס

$plot:$ \vDash \left\{ {p\left[ {x \leqslant e} \right]} \right\}x: = e\left\{ p \right\}$$

אם החישוב התחיל במצב $plot:$\sigma $$ כך שמתקיים $plot:$\sigma \vDash p\left[ {x \leftarrow e} \right]$$ אז המצב הסופי $plot:$\sigma '$$ יספק את plot:$p$ .

לפי למת החישובים, החישוב היחיד שיש להשמה הוא החישוב הבא:

$plot:$\left\langle {x: = e,\sigma } \right\rangle \to \left\langle {E,\sigma \left[ {x \leftarrow e} \right]} \right\rangle $$

צריך להוכיח כי $plot:$\sigma \vDash p\left[ {x \leftarrow e} \right] \to \sigma \left[ {x \leftarrow e} \right] \vDash p$$ . ביטוי זה נכון לפי המשפט מלוגיקה.

כעת נבדוק עבור plot:$skip$ : $plot:$ \vDash \left\{ p \right\}skip\left\{ p \right\}$$

נשתמש שוב בלמת החישובים, ונראה כי צריך להוכיח: $plot:$\sigma \vDash p \to \sigma \vDash p$$ , ביטוי שהוא נכון.

הוכחת כללי ההיסק

הרכבה סדרתית (SEQ):

נתון: $plot:$ \vDash \left\{ p \right\}{S_1}\left\{ r \right\}, \vDash \left\{ r \right\}{S_2}\left\{ q \right\}$$

צ"ל: $plot:$ \vDash \left\{ p \right\}{S_1};{S_2}\left\{ q \right\}$$

נשאל את עצמנו איזה סוג חישובים יש להרכבה סידרתית לפי למת החישובים. ישנם חישובים מתבדרים וישנם חישובים עוצרים. המקרה בו אנו מתעניינים עבור נכונות חלקית הוא מקרה שבו גם $plot:${S_1}$$ וגם $plot:${S_2}$$ עוצרים. עפ"י למת החישובים מתקיים $plot:${C_0}\xrightarrow{*}\left\langle {{S_2},{\sigma _1}} \right\rangle \xrightarrow{*}\left\langle {E,{\sigma _1}^\prime } \right\rangle $$ .

החלק $plot:${C_0}\xrightarrow{*}\left\langle {{S_2},{\sigma _1}} \right\rangle $$ מתאים לחישוב סופי של $plot:${S_1}$$ מלבד תוספת בכל קונפיגורציה.

עפ"י הנתון:

$plot:$\left( * \right) & \sigma \vDash p \Rightarrow \,{\sigma _1} \vDash r$$

$plot:$\left\langle {{S_2},{\sigma _1}} \right\rangle \xrightarrow{*}\left\langle {E,\sigma '} \right\rangle $$ הוא חישוב של $plot:${S_2}$$ ולכן עפ"י הנתון:

$plot:$\left( {**} \right) & {\sigma _1} \vDash r \Rightarrow \sigma ' \vDash q$$

מ- $plot:$\left( * \right)$$ ומ- $plot:$\left( {**} \right)$$ נסיק ש- $plot:$\sigma \vDash p \Rightarrow \sigma ' \vDash q$$ כנדרש.

לולאה (REP):

נתון: $plot:$ \vDash \left\{ {p \wedge B} \right\}S\left\{ p \right\}$$

צ"ל: $plot:$ \vDash \left\{ p \right\}{\text{while }}B{\text{ do }}S{\text{ od}}\left\{ {p \wedge \neg B} \right\}$$

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

$plot:${C_0}\xrightarrow{*}\left\langle {{S_0},{\sigma _1}} \right\rangle \xrightarrow{*}...\xrightarrow{*}\left\langle {E,{\sigma _k}} \right\rangle $$ . נסמן ב- $plot:${C_i} = \left\langle {while...,{\sigma _i}} \right\rangle $$ . אנו יודעים כי עבור $plot:$0 \leqslant i < k$$ מתקיים $plot:${\sigma _i} \vDash B$$ וכן כי $plot:${\sigma _k}\not \vDash B$$ .

באינדוקציה על מספר ביצועי החוג, נראה כי לכל $plot:$i \leqslant k$$ מתקיים $plot:${\sigma _i} \vDash p$$ , בתנאי ש- $plot:${\sigma _0} \vDash p$$ .

בסיס: צ"ל כי $plot:${\sigma _0} \vDash p$$ . זה נכון מכיוון שזה נתון.

צעד: נניח כי $plot:${\sigma _m} \vDash p$$ . נראה כי $plot:${\sigma _{m + 1}} \vDash p$$ עבור $plot:$m + 1 \leqslant k$$ .

על פי $plot:$ \vDash \left\{ {p \wedge B} \right\}S\left\{ p \right\}$$ אז לכל $plot:$\sigma ,\sigma '$$ כך שהחישוב של plot:$S$ מתחיל ב- $plot:$\sigma $$ ומסתיים ב- $plot:$\sigma '$$ מתקיים $plot:$\sigma \vDash p \wedge B \Rightarrow \sigma ' \vDash p$$ . מכאן המסקנה $plot:${\sigma _{m + 1}} \vDash p$$ .

עבור $plot:${\sigma _k}$$ , מתקיים כי $plot:${\sigma _k} \vDash p$$ על פי ההוכחה באינדוקציה. $plot:${\sigma _k} \vDash \neg B$$ ולכן קיבלנו את מה שצריך להוכיח.