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

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

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

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\}$ נפעל כמו שהגדרנו בטכניקה עבור כלל ההצבה, ונקבל:

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

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

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

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

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

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

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

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

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

כלל הסק עבור ifplot:$:\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\}$

נבחר את הטענה הנכונה הבאה:

plot:$1.\,\{ \underbrace {true}_p \wedge \underbrace {true}_B\} x: = x + 1\{ \underbrace {true}_p\} $

נפעיל REP:

plot:$2.\left\{ {true} \right\}{\text{while}}\,{\text{true}}\,{\text{do}}\,x: = x - 1\,\,{\text{od}}\left\{ {true \wedge false} \right\}$

נשתמש פעמיים באקסיומת ARITH:

plot:$\begin{gathered}   3.\,true \wedge false \to x = 0 \wedge false \hfill \\   4.\,x = 0 \to true \hfill \\ \end{gathered} $

נפעיל CONS על 2,3,4 ונקבל את הטענה אותה אנו מעוניינים להוכיח.

צריך לשים לב כי לא הראנו כי הוספת CONS גרמה למערכת להיות שלמה. הראנו כי הבעיה שהיתה קיימת לפני הוספת CONS (לא יכולנו להוכיח טענה נכונה) נפתרה.

תגיות המסמך:

לפרק הקודם5.1.4.1. אקסיומות
לפרק הבא5.1.4.3. משפט הנאותות של H
אין תגובות!
שיתוף:
| עוד