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