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

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

5.1.4.5. קצת פרקטיקה

איך בפועל אנחנו מוכיחים תוכניות במערכת ההוכחה H? נציג את דרך העבודה.

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

בהנתן תוכנית P, טענה התחלתית $plot:${q_1}$$ וטענה סופית $plot:${q_2}$$ , הרי שהשורה האחרונה בהוכחה שלנו תהיה $plot:$\left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$$ . כדי להוכיח את התוכנית נרצה לרשום סדרת כללי הוכחה המתחילים באקסיומות, ובהמשכם אקסיומות וכללי היסק, עד להגעה לתוצאה הסופית.

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

בהנתן תוכנית – נוח לרוב להתחיל בלולאות. אנחנו לוקחים לולאה ורושמים אותה כשלב בהוכחה. אם נסתכל על כלל REP, נשים לב כי plot:$p$ היא השמורה של הלולאה. נחשוב על שמורה עבור הלולאה שלנו, ובעזרתה נרכיב את הצעד בהוכחה הכולל את REP. זהו החלק הכי יצירתי לרוב בהוכחת HOARE שהיא מאוד טכנית. איך נמצא שמורה אם היא לא ברורה? דרך מומלצת היא לבצע מספר איטרציות של הלולאה, ולהרגיש מה קורה – איזה ערכים מקיימים חוקיות ביניהם. זו תהיה בחירה טובה כשמורה.