הוכחת נכונות של שירותים

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

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

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

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

נתחיל בהוכחת הנכונות של min1, השירות הראשון שבתוכנית המצורפת. הפעולה הראשונה של השירות היא להגדיר את המשתנה m ולאחסן בו את תוצאת החלוקה של 1 ב-0. התוצאה היא אינסוף. את ההוכחה נשלים בעזרת טענת עזר: הערך של המשתנה בסיום כל איטרציה של לולאת ה-for הוא הערך המינימלי מבין איברי המערך שהלולאה כבר עברה עליהם. ברור שהלולאה מבצעת לפחות איטרציה אחת, מכיון שתנאי הקדם מבטיח שהקלט לא יהיה null ושאורכו אחד לפחות. ברור שהטענה נכונה אחרי האיטרציה הראשונה, מכיון שבאיטרציה הזו אנו קובעים את m להיות הערך הקטן מבין הערך הראשון שהלולאה מחזירה ובין הערך ההתחלתי, אינסוף. מכיון שבמערך יש רק מספרים, אחרי האיטרציה הראשונה הערך של m הוא הערך הראשון שהוחזר על ידי הלולאה. הנכונות של הטענה במקרה הכללי נובעת באינדוקציה על מספר האיטרציות. מכיון שהלולאה מחזירה את כל איברי הלולאה, מטענת העזר נובע שהערך של m ביציאה מהלולאה הוא הערך המינימלי במערך, וזה אכן הערך שהשירות מוחזר, כנדרש בתנאי האחר.

נעבור להוכחת הנכונות של השירות הבא בתוכנית, min6. לשירות יש בדיוק את אותו חוזה כמו ל-min1. השירות ממומש בצורה פשוטה מאוד: על ידי קריאה לשירות עזר, minInRange. השירות minInRange מהווה ספק משנה של min6. ראשית אנו צריכים להוכיח שניתן לחשב את הארגומנטים שאנו מעבירים לספק המשנה. הארגומנט היחיד שצריך לחשב אותו הוא הארגומנט השלישי. מכיון שתנאי הקדם מבטיח שהקלט אינו null, הביטוי a.length הוא חוקי ולכן החישוב של הארגומנט יצליח. שנית, אנו צריכים לוודא שאנו מקיימים את תנאי הקדם של ספק המשנה. זה אכן מתקיים: הפסוק הראשון, השני, והרביעי של תנאי הקדם של minInRange מתקיימים משום שהם זהים לתנאי הקדם של min6; גם הפסוק השלישי מתקיים, כי a.length>0 מבטיח ש 0<=a.length-1, ולכן low<=high. השלב השלישי בהוכחה הוא להשתמש בתנאי האחר של ספק המשנה. תנאי האחר שלו מבטיח שבקריאה כזו, למצוא את המינימום בכל המערך, הוא יחזיר את המינימום, ולכן min6 יכול להחזיר את הערך הזה ולקיים בכך את תנאי האחר שלו עצמו.

כמובן שכעת צריך להוכיח ש-minInRange נכון. זה מורכב יותר משתי הדוגמאות הקודמות, מכיון שהשירות הזה רקורסיבי. הוא משמש כספק של עצמו! כאשר השירות רקורסיבי, הוכחת הנכונות היא אינדוקטיבית. אנו מניחים שהשירות נכון עבור ערך של high-low קטן מההפרש של הארגומנטים שהועברו, ומוכיחים שהוא נכון גם עבור הארגומנטים שהועברו. בסיס האינדוקציה הוא המקרה high-low==0, כלומר low==high. במקרה הזה ברור שהשירות מקיים את תנאי האחר, מכיון שהוא מחזיר את a[low]. הביטוי הזה חוקי מכיון ש-a אינו null ומכיון ש-low הוא בטווח האינדקסים של המערך (תנאי הקדם מבטיח את זה). כעת נניח את הנחת האינדוקציה ונוכיח את הנכונות של השירות. המפתח להוכחה הוא הערך של middle. אנו צריכים להראות לגביו שלוש טענות. טענה אחת היא שגם middle וגם middle+1 הם בטווח ערכי האינדקסים של המערך, כדי ששתי הקריאות הרקורסיביות ימלאו את תנאי הקדם. ברור ששני הערכים הללו הם לפחות אפס. הערכים הללו גם אינם גדולים מידי, מכיון ש:

middle == low + (high-low)/2 
       == 2*low/2 + (high-low)/2
       == (2*low + high - low)/2
       == (high + low)/2
       <  2*high/2
       == high 

כך שגם מתקיים middle+1<=high. הטענה השניה שצריך להראות היא ששני הטווחים low עד middle ו-middle+1 עד high, קטנים מהטווח low עד high. זה יאפשר לנו להפעיל את טענת האינדוקציה (ובאופן מעשי יותר, להיות בטוחים שהרקורסיה לא תהיה אינסופית). הטענה הזו מתקיימת לגבי הטווח הראשון מכיון שכבר הראינו ש middle<high, והיא מתקיימת לגבי הטווח השני מכיון ש middle+1>low. שתי הטענות הללו ביחד מבטיחות שהקריאות הרקורסיביות מקיימות את תנאי הקדם של השירות, ולכן הן יחזירו את המינימום בשני הטווחים. הטענה השלישית שאנו זקוקים לה היא ששני הטווחים ביחד מכסים בדיוק את הטווח low עד high. ברור כאן שזה נכון.זה מבטיח שהפעולה האחרונה של השירות, להחזיר את המינימום מבין שני הערכים שהוחזרו על ידי הקריאות הרקורסיביות, אכן מחזירה את המינימום בטווח כולו, כנדרש בתנאי האחר.

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

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

שאלות

1. הוכיחי את הנכונות של השירותים שהגדרנו בתוכנית שמלווה את הדיון ברקורסיית זנב.
2. הוכיחי את הנכונות של השירות sieveOfEratosthenes בדוגמה שליוותה את הדיון בהחזרת התייחסות משירות.