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

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

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

4.4.6. הוכחת עצירה של תוכניות בשפת PLF

נרצה כעת להראות כי תוכנית plot:$P$ נתונה עוצרת, כלומר: כל חישוב של התוכנית הוא סופי. הרעיון יהיה הצמדה של סדרה סופית יורדת אל כל חישוב. חשוב לשים לב כי מספיק להראות שכל לולאה היא סופית, ואין צורך להוכיח בבת אחת על כל התוכנית.

בכל תוכנית שנבדוק נחפש "מידה יורדת" כדי לחשוב על הפתרון. "מידה יורדת טובה" היא מידה שיורדת ממש בכל ביצוע של החוג.

לצורך המימוש נגדיר מושג חדש, קבוצה מבוססת היטב, בו נשתמש בכלל ההוכחה. ניתן להוכיח כי שימוש בקבוצת הטבעיים בלבד יספיק לנו לצרכי ההוכחה, אך לעתים נוח לבחור קבוצות אחרות.



תגיות המסמך:

לפרק הקודם4.4.5.3. נאותות ושלמות שיטת Floyd
לפרק הבא4.4.6.1. קבוצה מבוססת היטב
אין תגובות!
שיתוף:
| עוד