תכנות הוא יותר מקידוד

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

כשראיתי את זה לסלי למפורט (כן, אותו חבר מספרי הלימוד) מגיע לרוסיה ולא נותן דו"ח, אלא פגישת שאלות ותשובות, קצת נזהרתי. ליתר בטחון, לסלי הוא מדען בעל שם עולמי, המחבר של יצירות מכוננות בתחום המחשוב המבוזר, ואולי אתה גם מכיר אותו באותיות La ב-LaTeX - "Lamport TeX". הגורם המדאיג השני הוא הדרישה שלו: כל מי שמגיע חייב (לגמרי ללא תשלום) להאזין לכמה דיווחים שלו מראש, להעלות עליהם לפחות שאלה אחת, ורק אז להגיע. החלטתי לראות מה למפורט משדרת שם - וזה נהדר! זה בדיוק הדבר הזה, גלולת קישור קסומה לטיפול בזומבים. אני מזהיר אותך: הטקסט עלול לשרוף ברצינות את אלה שאוהבים מתודולוגיות סופר-זריזות ושלא אוהבים לבדוק את מה שכתבו.

לאחר ההברקות מתחיל למעשה תרגום הסמינר. קריאה מהנה!

כל משימה שתיקח על עצמך, אתה תמיד צריך לעבור שלושה שלבים:

• להחליט מה המטרה שאתה רוצה להשיג;
• להחליט איך בדיוק תשיג את המטרה שלך;
• תשיג את המטרה שלך.

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

• להחליט מה בדיוק התוכנית צריכה לעשות;
• לקבוע בדיוק כיצד עליו לבצע את משימתו;
• לכתוב את הקוד המתאים.

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

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

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

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

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

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

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

בואו נסתכל מקרוב על השלב הראשון: איזו בעיה התוכנית פותרת. כאן לרוב אנו מדגמים תוכנית כפונקציה שלוקחת קלט כלשהו ונותנת פלט כלשהו. במתמטיקה, פונקציה מתוארת בדרך כלל כקבוצה מסודרת של זוגות. לדוגמה, פונקציית הריבוע עבור מספרים טבעיים מתוארת כקבוצה {<0,0>, <1,1>, <2,4>, <3,9>, …}. תחום ההגדרה של פונקציה כזו הוא קבוצת האלמנטים הראשונים של כל זוג, כלומר, מספרים טבעיים. כדי להגדיר פונקציה, עלינו לציין את התחום והנוסחה שלה.

אבל פונקציות במתמטיקה אינן זהות לפונקציות בשפות תכנות. המתמטיקה הרבה יותר פשוטה. מכיוון שאין לי זמן לדוגמאות מורכבות, בוא נחשוב על אחת פשוטה: פונקציה ב-C או שיטה סטטית ב-Java שמחזירה את המחלק המשותף הגדול ביותר של שני מספרים שלמים. במפרט של שיטה זו נכתוב: מחושב GCD(M,N) לטיעונים M и Nאיפה GCD(M,N) - פונקציה שהתחום שלה הוא קבוצה של זוגות של מספרים שלמים, וערך ההחזר הוא המספר השלם הגדול ביותר שמחולק ב M и N. איך המציאות בהשוואה למודל הזה? המודל פועל עם מספרים שלמים, וב-C או Java יש לנו 32 סיביות int. מודל זה מאפשר לנו להחליט האם האלגוריתם נכון GCD, אבל זה לא ימנע שגיאות הצפה. זה ידרוש מודל מורכב יותר, שאין לו זמן.

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

בואו נראה איך ייראה השלב השני של האלגוריתם האוקלידי. אנחנו צריכים לחשב GCD(M, N). אנחנו מאתחלים M איך xו - N איך y, ואז להפחית שוב ושוב את הקטן מבין המשתנים הללו מהגדול עד שהם שווים. לדוגמה, אם M = 12ו - N = 18, נוכל לתאר את ההתנהגות הבאה:

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

ואם M = 0 и N = 0? האפס מתחלק בכל המספרים, ולכן אין המחלק הגדול ביותר במקרה זה. במצב זה צריך לחזור לשלב הראשון ולשאול: האם באמת צריך לחשב GCD למספרים לא חיוביים? אם זה לא הכרחי, אז אתה רק צריך לשנות את המפרט.

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

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

אנו משיגים בטיחות על ידי ציון תחילה קבוצה של מצבים ראשוניים אפשריים. ושנית, יחסים עם כל המדינות הבאות האפשריות עבור כל מדינה. בואו נתנהג כמו מדענים ונגדיר מצבים באופן מתמטי. קבוצת המצבים ההתחלתיים מתוארת על ידי הנוסחה, למשל, במקרה של האלגוריתם האוקלידי: (x = M) ∧ (y = N). לערכים מסוימים M и N יש רק מצב התחלתי אחד. הקשר עם המצב הבא מתואר על ידי נוסחה שבה המשתנים של המצב הבא נכתבים עם ראשוני, והמשתנים של המצב הנוכחי נכתבים ללא ראשי. במקרה של האלגוריתם האוקלידי, נעסוק בניתוק של שתי נוסחאות, באחת מהן x הוא הערך הגדול ביותר, ובשני - y:

במקרה הראשון, הערך החדש של y שווה לערך הקודם של y, ואנו מקבלים את הערך החדש של x על ידי הפחתת המשתנה הקטן מהגדול. במקרה השני, אנחנו עושים את ההיפך.

בואו נחזור לאלגוריתם האוקלידי. נניח שוב את זה M = 12, N = 18. זה מגדיר מצב התחלתי יחיד, (x = 12) ∧ (y = 18). לאחר מכן אנו מחברים את הערכים הללו לנוסחה למעלה ומקבלים:

הנה הפתרון האפשרי היחיד: x' = 18 - 12 ∧ y' = 12, ואנו מקבלים את ההתנהגות: [x = 12, y = 18]. באותו אופן, אנו יכולים לתאר את כל המצבים בהתנהגות שלנו: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].

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

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

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

כדי ליצור כלי עבודה, אתה צריך מתמטיקה פורמלית. איך הופכים מפרט רשמי? לשם כך נצטרך שפה פורמלית, למשל. TLA+. המפרט של האלגוריתם האוקלידי בשפה זו ייראה כך:

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

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

החיסרון העיקרי של TLA+ הוא שמדובר במתמטיקה, ומתכנתים ומדעני מחשב מפחדים ממתמטיקה. במבט ראשון זה נשמע כמו בדיחה, אבל, לצערי, אני אומר את זה במלוא הרצינות. עמית שלי בדיוק סיפר לי איך הוא ניסה להסביר TLA+ לכמה מפתחים. ברגע שהפורמולות הופיעו על המסך, עיניהם נעשו מיד זגוגיות. אז אם TLA+ מפחיד, אתה יכול להשתמש PlusCal, היא סוג של שפת תכנות צעצוע. ביטוי ב- PlusCal יכול להיות כל ביטוי TLA+, כלומר בעצם כל ביטוי מתמטי. בנוסף, ל- PlusCal יש תחביר עבור אלגוריתמים לא דטרמיניסטיים. מכיוון ש-PlusCal יכולה לכתוב כל ביטוי TLA+, הוא אקספרסיבי יותר באופן משמעותי מכל שפת תכנות אמיתית. לאחר מכן, PlusCal מורכב למפרט TLA+ קל לקריאה. זה לא אומר כמובן שהמפרט המורכב של PlusCal יהפוך לפשוט ב-TLA+ – רק שההתכתבות ביניהם ברורה, לא תופיע מורכבות נוספת. לבסוף, ניתן לאמת מפרט זה באמצעות כלי TLA+. באופן כללי, PlusCal יכולה לעזור להתגבר על פוביה ממתמטיקה; קל להבין אותה אפילו עבור מתכנתים ומדעני מחשב. פרסמתי עליו אלגוריתמים במשך זמן מה (בערך 10 שנים) בעבר.

אולי מישהו יתנגד לכך ש-TLA+ ו- PlusCal הן מתמטיקה, ומתמטיקה עובדת רק עם דוגמאות מומצאות. בפועל צריך שפה אמיתית עם טיפוסים, נהלים, חפצים וכדומה. זה לא נכון. הנה מה שכותב כריס ניוקומב, שעבד באמזון: "השתמשנו ב-TLA+ בעשרה פרויקטים גדולים, ובכל מקרה השימוש בו עשה הבדל משמעותי בפיתוח כי הצלחנו לתפוס באגים מסוכנים לפני שהם הגיעו לייצור, וכי זה נתן לנו את התובנה והביטחון שהיינו צריכים כדי להפוך לאגרסיביים אופטימיזציות של ביצועים מבלי להשפיע על האמת של התוכנית". לא פעם אפשר לשמוע שבשימוש בשיטות פורמליות אנחנו מקבלים קוד לא יעיל – בפועל הכל בדיוק הפוך. בנוסף, קיימת תפיסה שלא ניתן לשכנע מנהלים בצורך בשיטות פורמליות, גם אם מתכנתים משוכנעים בתועלת שלהן. וניוקומב כותב: "המנהלים דוחפים כעת בכל דרך אפשרית לכתוב מפרטים ב-TLA+, ומקצים זמן ספציפי לכך". אז כשמנהלים רואים ש+TLA עובד, הם מחבקים את זה. כריס ניוקומב כתב את זה לפני כחצי שנה (אוקטובר 2014), אבל עכשיו, עד כמה שידוע לי, משתמשים ב-TLA+ ב-14 פרויקטים, ולא ב-10. דוגמה נוספת מתייחסת לעיצוב של ה-XBox 360. מתמחה הגיע לצ'ארלס ת'אקר כתב מפרט עבור מערכת הזיכרון. הודות למפרט זה, נמצא באג שאחרת לא היה מתגלה ויגרום לכל XBox 360 לקרוס לאחר ארבע שעות של שימוש. מהנדסים מ-IBM אישרו שהבדיקות שלהם לא היו מזהות את הבאג הזה.

אתה יכול לקרוא עוד על TLA+ באינטרנט, אבל עכשיו בואו נדבר על מפרטים לא פורמליים. לעתים רחוקות אנחנו צריכים לכתוב תוכניות שמחשבות את המחלק הכי פחות משותף וכדומה. לעתים קרובות הרבה יותר אנו כותבים תוכניות כמו כלי המדפסת היפה שכתבתי עבור TLA+. לאחר העיבוד הפשוט ביותר, קוד TLA+ ייראה כך:

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

קחו דוגמה נוספת:

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

נראה שאם אין לנו הגדרה של אמת, אז המפרט חסר תועלת. אבל זה לא נכון. זה שאנחנו לא יודעים מה תוכנית צריכה לעשות לא אומר שאנחנו לא צריכים לחשוב איך היא אמורה לעבוד - להיפך, אנחנו צריכים להשקיע בה אפילו יותר מאמץ. המפרט חשוב כאן במיוחד. אי אפשר לקבוע את התוכנית האופטימלית להדפסה מובנית, אבל זה לא אומר שאסור לנו לעשות אותה בכלל, וכתיבת קוד כזרם תודעה אינו המקרה. בסופו של דבר כתבתי מפרט של שישה כללים עם הגדרות בצורה של הערות בקובץ Java. הנה דוגמה לאחד הכללים: a left-comment token is LeftComment aligned with its covering token. כלל זה כתוב, נניח, באנגלית מתמטית: LeftComment aligned, left-comment и covering token - מונחים עם הגדרות. כך מתמטיקאים מתארים מתמטיקה: הם כותבים הגדרות של מונחים ועל בסיסם יוצרים כללים. היתרון של מפרט זה הוא ששישה כללים הרבה יותר קלים להבנה ולניפוי באגים מאשר 850 שורות קוד. אני חייב לומר שכתיבת הכללים האלה לא הייתה קלה; לקח די הרבה זמן לנפות אותם. כתבתי קוד במיוחד למטרה זו שאמר לי באיזה כלל נעשה שימוש. מכיוון שבדקתי את ששת הכללים האלה עם כמה דוגמאות, לא הייתי צריך לנפות באגים ב-850 שורות קוד, והבאגים היו די קלים למצוא. ל-Java יש כלים מצוינים לכך. אם רק הייתי כותב את הקוד, זה היה לוקח לי הרבה יותר זמן והעיצוב היה באיכות ירודה יותר.

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

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

אבל למפרט הזה יש גם תכונות שמבדילות אותו ממפרטים אחרים. 95% מהמפרטים האחרים הם הרבה יותר קצרים ופשוטים:

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

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

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

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

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

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

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

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

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

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

תוכלו לקרוא עוד על TLA+ ו-PlusCal באתר מיוחד, לשם תוכלו להגיע מעמוד הבית שלי по ссылке. זה הכל בשבילי, תודה על תשומת הלב.

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

מקור: www.habr.com