3.3.1. הגדרה
תוכנית P היא נכונה חלקית (partially correct) ביחס למפרט
אם ורק אם לכל חישוב
של התוכנית P, המתחיל ממצב התחלתי
המספק את
, כלומר
, מתקיים שאם החישוב עוצר
אזי
מתקיים בסוף החישוב. ![plot:$\left(
{val\left( {\pi \left( {P,{\sigma _0}} \right)} \right) \vDash {q_2}\left(
{\bar x} \right)} \right)$](/documentResources/326/plot_354.png)
ניסוח מתמטי: ![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)$](/documentResources/326/plot_355.png)
מסקנה:
חישוב אינסופי מספק כל טענת נכונות חלקית.
שאלה: האם בניסוח המתמטי ניתן לוותר על
? התשובה היא לא. נניח כי
אינסופי, וכי
, נקבל
שזהו ביטוי
. נכונות חלקית צריכה להיות נכונה על חישוב לא עוצר,
ולכן יש צורך בחלק זה כדי להגדיר את הנכונות החלקית.
סימון לנכונות חלקית: ![plot:$\left\{ {{q_1}} \right\}P\left\{ {{q_2}}
\right\}$](/documentResources/326/plot_361.png)
סימונים קשורים נוספים:
הטענה
נכונה.
הטענה יכיחה ("ניתנת
להוכחה") במערכת ההוכחה D.
טענות:
- רק תוכנית שלעולם לא עוצרת מספקת את המפרט
.
- כל תוכנית מספקת את המפרט
.
כדי להסביר את
הטענות נתחיל מההגדרה: אם המצב לפני התוכנית מספק את
, אז אם
התוכנית עוצרת, אחרי התוכנית המצב הסופי יספק את
.
איזה מצב מספק את
?
אף מצב - ולכן
המפרט
מתקיים (באופן ריק) על כל תוכנית
P.
המצב ה-"מעניין"
יותר הוא המצב ההפוך:
.
אם המצב לפני
התוכנית מספק את true, אז אם התוכנית עוצרת המצב
יספק את
.
איזה מצב מספק את
? כל מצב.
איזה מצב מספק את
? אף
מצב.
ניתן להסיק ש-P לעולם לא עוצרת. כי אם כן, המצב היה מספק את
וזה לא יתכן.
לסיכום: באופן אינטואיטיבי, המפרט
מתאים לכל תוכנית שאינה עוצרת.