לאמץ את כוחן של שיטות פורמליות במסע הקידוד שלי: איך הפכתי לאוונגליסט דפני

בלוג 1חדשות מפתחיםיזם הסבר על בלוקצ’יין אירועים וכנסים לחץעלונים

הירשם לניוזלטר שלנו.

כתובת דוא”ל

אנו מכבדים את פרטיותך

HomeBlogDevelopers

לאמץ את כוחן של שיטות פורמליות במסע הקידוד שלי: איך הפכתי לאוונגליסט דפני

על ידי ConsenSys 22 בדצמבר 2020 הועלה ב 22 בדצמבר 2020

צילום מסך 2020 12 15 בשעה 6 46 32 אחר הצהריים 1

מאת ג’ואן פולר

אני רוצה להתחיל באומרו שאני כותב את הפוסט בבלוג בתקווה שאחרים יוכלו לחוות את רגע ההתגלות שהיה לי בזמן שלמדתי. דפני כחלק מהחקירה שלי אל שיטות פורמליות. יתר על כן, אני מקווה שפרסום זה ישמש כזרז לאחרים לראות בשיטות פורמליות כמיומנות קריטית והכרחית בארסנל של כל מי שכותב קוד. כחלק מ צוות אימות אוטומטי בתוך R&D ב- ConsenSys, אני משתמש בדפני לצורך אימות רשמי של מפרט שלב 0 של Ethereum 2, ואני רוצה לשתף מדוע אני מוצא את זה שימושי.

הרקע שלי

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

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

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

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

דוגמא ראשונה לדפני

כדוגמא פשוטה שקול את חלוקת המספר השלם של דיבידנד לא שלילי n על ידי מחלק חיובי d; 


n / d

מוצג להלן:

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

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

רגע ההתגלות שלי

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

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

במדריך זה רוסטן ליינו עובר שיטת SumMax שלוקחת שני מספרים שלמים, x ו- y, ומחזירה את הסכום והמקסימום, s ו- m בהתאמה. דוגמה זו פשוטה יחסית וקוד Dafny מוצג להלן.

הקלטים x ו- y מוגדרים כמספרים שלמים באמצעות הקלדה ואין צורך בתנאים מוקדמים אחרים. שלושת תנאי הפרסום מספקים בדיקות שהפלט אכן עומד במפרטים, כלומר ש- שווה ל- x + y, וכי m שווה ל- x או ל- y וכי m אינו עולה על x ו- y. לאחר מכן מוצגת שיטת SumMaxBackwards כתרגיל וכאן היא נהיית מעניינת יותר. המפרט הוא הפוך מ- SumMax, כלומר בהתחשב בסכום ובהחזר המרבי המספרים השלמים x ו- y. אוקי, כך שניסיון ראשון עשוי להיות עם אותן תנאי פוסט; שכן היחסים בין התשומות והפלט עדיין מתקיימים. אם אנו נותנים ל- x להיות המקסימום אז מעט אלגברה מהירה אומרת לנו ש- y צריך להיות שווה לסכום פחות המקסימום. הכנסת זה לעורך המקוון נותנת את הדברים הבאים.

צילום מסך 2020 12 15 בשעה 6 38 37 אחר הצהריים 1 צילום מסך 2020 12 16 בשעה 5 35 22 אחר הצהריים

זה לא מאמת. אז מה השתבש? נאמר לנו שתנאי שלא הוחזק ובאופן ספציפי התנאי שלאחר קו 3 (מבטיח x<= מ ‘ && y <= m) לא יכול להחזיק. במבט מקרוב אנו רואים שתנאי פוסט זה מציין ש- x <= m ו- y <= מ ‘ ובכן, אנו יודעים ש- x קטן או שווה ל- m כפי שקבענו שווה ל- x, ולכן המשמעות היא שה- y <= מ ‘חלק לא מאמת. איך זה יכול לקרות? האלגברה שלנו אמרה לנו ש- y: = s – m. נניח ש s הוא 5 ו- m הוא 3, אז y = 5 – 3 = 2 מה שמבטיח y <= m; אבל בואו נגיד שאנחנו קוראים לשיטה הזו עם s שווה ל- 5 ו- m שווה ל- 1. שום דבר לא ימנע מאיתנו לקרוא לשיטה עם פרמטרים של קלט אלה אבל לעשות זאת יגרום לבעיה כמו y = 5 – 1 = 4 ואז y > M. בעיקרון מה שאנחנו רואים כאן הוא שלמרות שפרמטר הקלט אמור להיות המקסימום של שני מספרים שלמים שיוצרים את הסכומים, אין שום דבר שיעצור אותנו לנסות לקרוא לשיטה עם קלט שאינו תקף. אלא אם כן נכלל תנאי מוקדם להגבלת התשומות של s ו- m למספרים שלמים תקפים שיגרמו לפלטים x ו- y העומדים במפרט, אז השיטה שלנו יכולה לייצר תוצאות שגויות. לאיזה קשר אנו זקוקים בין s ל- m כדי לספק תשומות תקפות? קצת יותר אלגברה מראה לנו ש- <= m * 2 כדי שיהיה פיתרון תקף של x ו- y. אם נוסיף זאת כתנאי מקדים, דפני יכול כעת לאמת את הקוד כפי שמוצג להלן. 

צילום מסך 2020 12 15 בשעה 6 46 32 אחר הצהריים 1 צילום מסך 2020 12 16 בשעה 5 37 39 אחר הצהריים

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

על מה אני עובד עכשיו

ובכן זה מביא אותי לסוף ההודעה שלי. אם תרצה לראות על מה אני עובד כרגע עם דפני, בדוק זאת ריפו של GitHub. אני חלק מצוות האימות האוטומטי בתוך R&D ב- ConsenSys ואנחנו משתמשים ב- Dafny לצורך אימות רשמי של מפרט שלב 0 של Ethereum 2. השימוש בשיטות פורמליות במרחב הבלוקצ’יין הוא תחום מחקר חדש ומלהיב שאומץ על ידי ConsenSys, ואעודד את כל מי שמעוניין ללמוד עוד על Eth 2.0 לבדוק את המשאבים הזמינים ברשימת הפרויקט שלנו..

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

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me
Like this post? Please share to your friends:
Adblock
detector
map