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

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

3.3.1. הגדרה

תוכנית P היא נכונה חלקית (partially correct) ביחס למפרט $plot:$ < {q_1}\left( {\bar x} \right),{q_2}\left( {\bar x} \right) > $$ אם ורק אם לכל חישוב $plot:$\pi $$ של התוכנית P, המתחיל ממצב התחלתי $plot:${\sigma _0}$$ המספק את $plot:${q_1}\left( {\bar x} \right)$$ , כלומר $plot:${\sigma _0} \vDash {q_1}\left( {\bar x} \right)$$ , מתקיים שאם החישוב עוצר $plot:$\left( {val\left( {\pi \left( {P,{\sigma _0}} \right)} \right) \ne \bot } \right)$$ אזי $plot:${q_2}\left( {\bar x} \right)$$ מתקיים בסוף החישוב. $plot:$\left( {val\left( {\pi \left( {P,{\sigma _0}} \right)} \right) \vDash {q_2}\left( {\bar x} \right)} \right)$$

ניסוח מתמטי: $plot:${\sigma _0} \vDash {q_1}\left( {\bar x} \right) \wedge Val\left( {\pi \left( {P,{\sigma _0}} \right)} \right) \ne \bot \to Val\left( {\pi \left( {P,{\sigma _0}} \right)} \right) \vDash {q_2}\left( {\bar x} \right)$$

מסקנה: חישוב אינסופי מספק כל טענת נכונות חלקית.

שאלה: האם בניסוח המתמטי ניתן לוותר על $plot:$Val\left( {\pi \left( {P,{\sigma _0}} \right)} \right)$$ ? התשובה היא לא. נניח כי $plot:$\pi $$ אינסופי, וכי $plot:${\sigma _0} \vDash {q_1}$$ , נקבל $plot:$true \Rightarrow false$$ שזהו ביטוי plot:$false$ . נכונות חלקית צריכה להיות נכונה על חישוב לא עוצר, ולכן יש צורך בחלק זה כדי להגדיר את הנכונות החלקית.

סימון לנכונות חלקית: $plot:$\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$$

סימונים קשורים נוספים:

$plot:$ \vDash \left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$$ הטענה נכונה.
$plot:${ \vdash _D}\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$$ הטענה יכיחה ("ניתנת להוכחה") במערכת ההוכחה D.

טענות:

רק תוכנית שלעולם לא עוצרת מספקת את המפרט $plot:$\left\{ {true} \right\}P\left\{ {false} \right\}$$ .
כל תוכנית מספקת את המפרט $plot:$\left\{ {false} \right\}P\left\{ {true} \right\}$$ .

כדי להסביר את הטענות נתחיל מההגדרה: אם המצב לפני התוכנית מספק את $plot:${q_1} = false$$ , אז אם התוכנית עוצרת, אחרי התוכנית המצב הסופי יספק את $plot:${q_2} = true$$ .

איזה מצב מספק את plot:$false$ ?

אף מצב - ולכן המפרט $plot:$\left\{ {false} \right\}P\left\{ {true} \right\}$$ מתקיים (באופן ריק) על כל תוכנית P.

המצב ה-"מעניין" יותר הוא המצב ההפוך: $plot:$\left\{ {true} \right\}P\left\{ {false} \right\}$$ .

אם המצב לפני התוכנית מספק את true, אז אם התוכנית עוצרת המצב יספק את plot:$false$ .

איזה מצב מספק את plot:$true$ ? כל מצב. איזה מצב מספק את ? אף מצב.

ניתן להסיק ש-P לעולם לא עוצרת. כי אם כן, המצב היה מספק את וזה לא יתכן.

לסיכום: באופן אינטואיטיבי, המפרט $plot:$\left\{ {true} \right\}P\left\{ {false} \right\}$$ מתאים לכל תוכנית שאינה עוצרת.