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

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

5.1.4.2. כללי הסק

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

כלל הסק עבור הרכבה סדרתית $plot:$:\left( {SEQ} \right)$$ $plot:\[\frac{{\left\{ p \right\}{s_1}\left\{ r \right\}\, & \,\left\{ r \right\}{s_2}\left\{ q \right\}}}{{\left\{ p \right\}{s_1};{s_2}\left\{ q \right\}}}\]$

דוגמא לשימוש: רוצים להוכיח את הטענה הבאה:

$plot:${ \vdash _h}\left\{ {x = X \wedge y = Y} \right\}z: = x;x: = y;y: = z\left\{ {x = Y \wedge y = X} \right\}$$

שימוש באקסיומת ההצבה: מסתכל על הביטוי מצידו הימני: $plot:$y: = z\left\{ {x = Y \wedge y = X} \right\}$$ נפעל כמו שהגדרנו בטכניקה עבור כלל ההצבה, ונקבל:

$plot:$\left( {ASS} \right)\,\,\,\left\{ {x = Y \wedge z = X} \right\}y: = z\left\{ {x = Y \wedge y = X} \right\}$$

ניקח את הביטוי מצד שמאל, ונפעיל שוב את אקסיומת ההצבה עם ההצבה plot:$x: = y$ .

$plot:$\left( {ASS} \right)\,\,\,\left\{ {y = Y \wedge z = X} \right\}x: = y\left\{ {x = Y \wedge z = X} \right\}$$

כעת נשתמש בהרכבה SEQ לשרשור התוצאות:

$plot:$(SEQ)1,2\,\,\,\left\{ {y = Y \wedge z = X} \right\}x: = y;y: = z\left\{ {x = Y \wedge y = X} \right\}$$

נשתמש שוב באקסיומת ההצבה כאשר מימין אנו שמים את הצד השמאלי של (3).

$plot:$\left( {ASS} \right)\,\,\,\left\{ {y = Y \wedge x = X} \right\}z: = x\left\{ {y = Y \wedge z = X} \right\}$$

לסיום נבצע שוב SEQ והוכחנו את הטענה שהתבקשנו להוכיח.

$plot:\[(SEQ)3,4\,\,\,\left\{ {y = Y \wedge x = X} \right\}z: = x;x: = y;y: = z\left\{ {x = Y \wedge y = X} \right\}\]$

כלל הסק עבור if $plot:$:\left( {COND} \right)$$ $plot:\[\frac{{\left\{ {p \wedge B} \right\}{S_1}\left\{ q \right\}\,\, & & \,\left\{ {p \wedge \neg B} \right\}{S_2}\left\{ q \right\}}}{{\left\{ p \right\}if\,B\,then\,\,{S_1}\,else\,{S_2}\,\,\,fi\,\,\left\{ q \right\}}}\,\]$

הכלל נאות: כל חישוב של plot:$if$ הוא חישוב של $plot:${S_1}$$ או של $plot:${S_2}$$ ובשני המקרים הוכחנו שהמצב הסופי (אם קיים) מספק את plot:$q$ .

כלל הסק עבור while $plot:$:\left( {REP} \right)$$ $plot:\[\frac{{\left\{ {p \wedge B} \right\}S\left\{ p \right\}}}{{\left\{ p \right\}while\,\,B\,\,do\,\,S\,\,\,od\,\left\{ {p \wedge \neg B} \right\}}}\]$

plot:$p$ היא האינואריאנטה של הלולאה. כלל זה חלש מידי עבור שלמות! קיימות טענות נכונות במערכת שלא נוכל להוכיח ולכן מוסיפים כלל נוסף – CONS.

כלל הסק $plot:$:\left( {CONS} \right)$$ $plot:$\frac{{p \to {p_1}\, & \left\{ {{p_1}} \right\}S\left\{ {{q_1}} \right\}\,\, & {q_1} \to q}}{{\left\{ p \right\}S\left\{ q \right\}}}$$ כאשר plot:$p,q$ הן טענות מסדר ראשון.

דוגמא לאי-שלמות ללא CONS:

נביט בטענה הבאה: $plot:$\left\{ {x = 0} \right\}\,\,{\text{while}}\,\,{\text{true}}\,\,{\text{do}}\,\,x: = x - 1\,\,\,{\text{od}}\,\,\,\left\{ {x = 0 \wedge {\text{false}}} \right\}$$

הטענה אומרת "אם יודעים כי plot:$x
= 0$ ואז מבצעים $plot:${\text{while}}\,\,{\text{true}}\,\,{\text{do}}\,\,x: = x - 1\,\,\,{\text{od}}$$ נרצה שיתקיים $plot:$x = 0 \wedge {\text{false}}$$ ".

הטענה נכונה בגלל שאנו מדברים על נכונות חלקית, והלולאה לעולם אינה עוצרת. אנו רוצים להוכיח את הטענה הנכונה, והדרך היחידה ללא plot:$CONS$ לקבל טענת while היא ע"י plot:$REP$ . נוכיח אם כך את מה שמעל הקו של טענת plot:$while$ :

$plot:$\left\{ {x = 0 \wedge true} \right\}\,\,x: = x - 1\,\,\left\{ {x = 0} \right\}$$

טענה זו אינה נכונה ומכיוון שמע' ההוכחה נאותה לא נוכל להוכיח אותה. קיבלנו שלילה של השלמות, כי לא ניתן להוכיח את הטענה ממנה התחלנו, שהיא טענה נכונה.

נראה כעת איך מוכיחים את הטענה כאשר CONS כן חלק ממערכת ההוכחה.

כאמור, אנו רוצים להוכיח $plot:$\left\{ {x = 0} \right\}\,\,{\text{while}}\,\,{\text{true}}\,\,{\text{do}}\,\,x: = x - 1\,\,\,{\text{od}}\,\,\,\left\{ {x = 0 \wedge {\text{false}}} \right\}$$