4.4.5.3. נאותות ושלמות שיטת Floyd
משפט הנאותות של F –
(מערכת ההוכחה של פלויד):
אם מתקיים
אז
. במילים: אם ניתן להוכיח את הטענה במערכת
ההוכחה Floyd, אז הטענה נכונה.
על מנת להוכיח את המשפט, נציג למת עזר:
למה: אם
אזי לכל חישוב
של P, שמתחיל ממצב
שמקיים:
, אם החישוב מגיע לנקודת חתך
במצב
אזי
.
כלומר: אם ניתן במערכת ההוכחה להוכיח את
אז כל חישוב שמתחיל ממצב
ומספק את תנאי ההתחלה, בהגיעו לנקודת החתך במצב
כלשהו, מצב זה מספק את התנאי של נקודת החתך.
הוכחת הלמה תעשה באינדוקציה על מספר
נקודות החתך בהן עבר החישוב:
בסיס: חישוב
שעבר בנקודת חתך אחת:
. מתקיים
כי נתון שמתקיים
.
צעד: ניקח
מסלול בו
נקודות חתך. הנחת האינדוקציה היא:
וכן מתקיים
(המסלול עביר). צריך להוכיח כי מתקיים:
.
קצת לוגיקה: בעצם מהנתונים מתקיימת טענת
הנכונות:
![plot:${\sigma
_i} \vDash \left( {{I_{{l_i}}}\left( {\bar x} \right) \wedge {R_{i \to i +
1}}\left( {\bar x} \right) = {I_{{l_{1 + 1}}}}\left[ {{T_{{l_i} \to {l_{i +
1}}}}\left( {\bar x} \right)} \right]} \right)$](/documentResources/326/plot_616.png)
מטענת הנכונות מתקיים
. זהו אינו הביטוי המדוייק אותו אנו צריכים להוכיח, לכן נשתמש
במשפט מלוגיקה:
תזכורת: מתקיים תמיד ![plot:$S\left[
{x \leftarrow s\left( e \right)} \right] \vDash \varphi \Leftrightarrow s \vDash \varphi \left[ {x
\leftarrow e} \right]$](/documentResources/326/plot_618.png)
זוהי השמה חדשה (אצלנו = מצב חדש) שזהה ל-
חוץ מהערך של
שהוא
,
כאשר
זו נוסחה בה החלפנו את
בביטוי
.
על סמך המשפט בלוגיקה נסיק:
.
העברנו שינויים בנוסחה לשינויים במצב.
מתקיים
כנדרש.
הוכחת משפט הנאותות:
נניח כי מתקיים
, אזי המצבים האפשריים:
- אם חישוב
של
תוכנית אינו עוצר, אז אין דרישה עבורו בנכונות חלקית.
- חישוב
שמתחיל
מ-start ממצב
כך ש-
עוצר. על סמך הלמה ב-halt
מתקיימת הטענה
.
משפט השלמות עבור F: אם
מתקיים
אז
. כלומר ניתן למצוא נקודות חתך וטענות אינווריאנטיות
שמספקות את תנאי הנכונות.