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

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

3. הוכחת נכונות של תוכניות

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

מרכיבים נדרשים למערכת ההוכחה של תוכנית:

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

המטרה שלנו: בהינתן תוכנית P, נרצה להוכיח שהתוכנית מקיימת את המפרט שלה.

דוגמא למפרט המתאר תוכניות מיון: $plot:$a[i] \leqslant a[j]$$ $plot:$\forall 0 \leqslant i,j \leqslant n$$

הגדרה: תהי תוכנית P ומפרט $plot:$\varphi $$ . נאמר כי plot:$P$ נכונה ביחס ל- $plot:$\varphi $$ אם מתקיים $plot:$P \vDash \varphi $$

(P מספק את $plot:$\varphi $$ ).

איך נבדוק ספיקות של תוכנית?

תוכנית עם מספר מצבים סופי: נעבור על כל המצבים ונבדוק את ספיקות התוכנית.
תוכנית עם מספר מצבים אינסופי (שהוא טרנספורמציית קלט-פלט): דרושה מערכת הוכחה.

נטפל בתוכניות דטרמיניסטיות בלבד, כלומר ישנו חישוב יחיד לכל פלט $plot:$ \Leftarrow $$ לכל קלט יש תוצאה אחת לכל היותר. (לכל היותר = התוכנית יכולה לא לעצור כלל).