5.1.4.5. קצת פרקטיקהאיך בפועל אנחנו מוכיחים תוכניות במערכת ההוכחה H? נציג את דרך העבודה. אנו מקבלים תוכנית בשפת while וטענות שאנחנו רוצים לבדוק אם הן מתקיימות לגבי התוכנית. בהנתן תוכנית P, טענה התחלתית נשים לב שעם תחילת ההוכחה, אנחנו יודעים מה אנחנו רוצים לקבל – את השורה האחרונה. אנחנו צריכים לקבוע מה היה קודם. נשים לב לנקודה חשובה נוספת: בכללי ההיסק שנציג הזהות חייבת להיות סינטטקטית, ולא רק סמנטית. ההוכחה שלנו היא הוכחה בלוגיקה. בהנתן תוכנית – נוח לרוב להתחיל
בלולאות. אנחנו לוקחים לולאה ורושמים אותה כשלב בהוכחה. אם נסתכל על כלל REP,
נשים לב כי בשלב הבא בהוכחה, לאחר שכתבנו את REP, נכתוב את השלב שלפני REP – למעשה את הביטוי שמעל הקו בכלל ההיסק. זהו הביטוי שאנחנו רוצים להוכיח, כדי שה-REP יתקדם. בכל שלב בתהליך ההוכחה אנחנו מסתכלים מה היה צריך לקרוא כדי שהביטוי בשלב הנוכחי יתקיים, ורושמים את הביטוי הנדרש, עד שאנחנו מגיעים אל האקסיומות.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |