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

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

5.1.5. מערכת H* להוכחת $plot:$\left\langle p \right\rangle S\left\langle q \right\rangle $$

במערכת זו, מלבד כלל plot:$REP$ של מערכת H, נאמץ את כל הכללים כמו שהם תוך כדי החלפת $plot:$\left\{ {} \right\}$$ ב- $plot:$\left\langle {} \right\rangle $$ . כלל REP החדש: נשתמש ב- $plot:$\mathbb{N}$$ עם הסדר הרגיל (בתור $plot:$\left( {w, < } \right)$$ ). נקבע טענות $plot:\[p\left( {\bar x,n} \right)\]$ כאשר $plot:$\bar x$$ משתני התוכנית ו- plot:$n$ מעל הטבעיים (כולל 0):

$plot:\[\frac{{\left( {p\left( {\bar x,n} \right) \wedge n > 0} \right) \to B & & \,\,\,\left\langle {p\left( {\bar x,n} \right) \wedge \left( {n > 0} \right)} \right\rangle S\left\langle {p\left( {\bar x,n - 1} \right)} \right\rangle & & \,\,\,p\left( {\bar x,0} \right) \to \neg B}}{{\left\langle {\exists n,p\left( {\bar x,n} \right)} \right\rangle \,\,{\text{while}}\,\,B\,\,{\text{do}}\,\,S\,\,{\text{od}}\,\,\left\langle {p\left( {\bar x,0} \right)} \right\rangle }}\]$

משפט הנאותות: $plot:${ \vdash _{{H^*}}}\left\langle {{p_1}} \right\rangle S\left\langle {{q_1}} \right\rangle \Rightarrow \,\, \vDash \left\langle {{p_1}} \right\rangle S\left\langle {{q_1}} \right\rangle $$

נוכיח את משפט הנאותות רק עבור מקרה פרטי: עבור תוכנית $plot:$S = while\,\,B\,\,do\,\,S'\,\,od$$ כאשר plot:$S'$ אינו מכיל חוגים.

הוכחה:

התוכנית plot:$S$ הינה ללא חוגים, לפי הנאותות של H. כמו כן: $plot:$S = while\,\,B\,\,do\,\,S'\,\,od$$ . לפי למת החישובים, ביצוע S שאינו עוצר נראה כך: $plot:$\left\langle {S,{\sigma _0}} \right\rangle \xrightarrow{*}\left\langle {S,{\sigma _1}} \right\rangle \xrightarrow{*}...$$ כאשר $plot:$\forall i,{\sigma _i} \vDash B$$ .

כדי להוכיח נאותות, נביט איך נראית הוכחה של WHILE, ונראה כי הנאותות מתקיימת:

1. $plot:$p\left( n \right) \wedge \left( {n > 0} \right) \to B$$ (נתון מהנאותות)

2. $plot:$\left\langle {p\left( n \right) \wedge n > 0} \right\rangle S\left\langle {p\left( {n - 1} \right)} \right\rangle $$ (נתון מהנאותות)

3. $plot:$p\left( 0 \right) \to \neg B$$ (נתון מהנאותות)

4. $plot:$\left\langle {\exists n,\,p\left( n \right)} \right\rangle \,\,while\,\,B\,\,do\,\,S'\,od\,\left\langle {p\left( 0 \right)} \right\rangle $$ $plot:$\left( {{\text{REP }}1,2,3} \right)$$

5. $plot:${p_1} \to \exists n,\left( {p\left( n \right)} \right)$$

6. $plot:$p\left( 0 \right) \to {q_1}$$

7. $plot:$\left\langle {{p_1}} \right\rangle \,\,while\,\,B\,\,do\,\,S'\,od\,\left\langle {{q_1}} \right\rangle $$ $plot:$\left( {{\text{CONS}}\,\,{\text{4,5,6}}} \right)$$

נסיק שלא קיים חישוב אינסופי כי חישוב שמתחיל מ- $plot:$\sigma $$ $plot:$\left( {\sigma \vDash {p_1}} \right)$$ ע"ס plot:$S$ : $plot:$\sigma \vDash {\exists _n}p\left( n \right)$$ לכן קיים plot:$k$ כך ש- $plot:$\sigma \vDash p\left( k \right)$$ .

ניתן להראות באינדיקציה ש- $plot:$p\left( 0 \right)$$ מתקיים תוך plot:$k$ צעדים עבור $plot:$\sigma '$$ $plot:$\sigma ' \vDash p\left( 0 \right) \Rightarrow \sigma ' \vDash \neg B$$ (עפ"י 3) ולכן יש עצירה.

תרגיל

המטרה: לנסח כלל plot:$REP$ בו הירידה היא לאו דווקא ב-1 והעצירה לאו דווקא ב-0.

פתרון 1: נגדיר אוסף כללים $plot:$RE{P^*}\left( c \right)$$ - כלל לכל קבוע טבעי אפשרי plot:$c$ :

$plot:$RE{P^*}\left( c \right):\,\,\,\,p\left( {\bar x,n} \right) \wedge \left( {n > c} \right) \to B$$

$plot:$\frac{\begin{gathered} \left\langle {p\left( {\bar x,n} \right) \wedge \left( {n > c} \right)} \right\rangle S\left\langle {\exists n':p\left( {x,n'} \right) \wedge c \leqslant n' \leqslant n} \right\rangle \hfill \\ p\left( {\bar x,c} \right) \to \neg B \hfill \\ \end{gathered} }{{\left\langle {\exists n,\,p\left( {X,n} \right) \wedge \left( {n \geqslant c} \right)} \right\rangle \,\,while\,\,B\,\,do\,\,S\,\,od\,\,\left\langle {p\left( {\bar x,c} \right)} \right\rangle }}$$

פתרון 2:

$plot:$\frac{\begin{gathered} \left\langle {p\left( n \right) \wedge n > 0 \wedge B} \right\rangle S\left\langle {\exists n' < n\,,\,p\left( {n'} \right)} \right\rangle \hfill \\ p\left( 0 \right) \to \neg B \hfill \\ \end{gathered} }{{\left\langle {\exists n,p\left( n \right)} \right\rangle \,while\,\,B\,\,do\,\,S\,\,od\,\left\langle {\exists n',\,p\left( {n'} \right) \wedge \neg B} \right\rangle }}$$

תרגיל

סעיף א':

נשנה את מערכת ההוכחה ונראה כיצד השינוי משפיע על המערכת. נשנה את כלל REP על ידי שנבטל את ההנחה $plot:\[\left( {p\left( {\bar x,n} \right) \wedge n > 0} \right) \to B\]$ . מה ניתן להגיד כעת על מערכת ההוכחה?

כלל REP החדש:

מבטיח שאם והדרישה מתקיימת אז נכנסים אל הלולאה.
יכול להיות ש- וגם B הוא false. מכאן: לא מבטיחים עצירה של הלולאה ב-0. הלולאה יכולה לעצור כאשר .
הכלל עדיין מבטיח את עצירת הלולאה!

האם המערכת שלמה? התשובה היא כן – כי החלשנו את התנאי. השלמות לא תפגע. לעומת זאת, הנאותות איננה נשמרת.

סעיף ב':

כעת נשנה את הכלל השני ב-REP להיות $plot:\[\left\langle {p\left( {\bar x,n} \right)} \right\rangle S\left\langle {p\left( {\bar x,n - 1} \right)} \right\rangle \]$ במקום $plot:\[\left\langle {p\left( {\bar x,n} \right) \wedge \left( {n > 0} \right)} \right\rangle S\left\langle {p\left( {\bar x,n - 1} \right)} \right\rangle \]$ . איך הנאותות והשלמות של המערכת יושפעות במקרה זה?

במקרה זה אנו פוגעים בשלמות אך לא בנאותות. נשים לב שבעת ההוכחה נצטרך להוכיח כעת יותר: נצטרך להוכיח שהטענה מתקיימת גם עבור כל n שלילי, ולא רק עבור n גדול מ-0.