בטיחות סוג

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

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

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

הגדרות

באופן אינטואיטיבי, תקינות הטיפוס נתפסת על ידי האמירה של רובין מילנר:

תוכניות מוגדרות היטב מבחינת סוגים אינן יכולות "לעשות טעויות".

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

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

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

התקדמות

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

שימור (או הפחתת נושא)

לאחר כל שלב הערכה, הסוג של כל ביטוי נשאר זהה (כלומר, הסוג שלו "נשמר").

קשר לצורות בטיחות אחרות

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

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

שפות עם בטיחות סוג חזקה וחלשה

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

ניהול זיכרון ובטיחות סוג

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

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

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

בטיחות סוג בשפות מונחות עצמים

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

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

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

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

ראו גם

• מערכת טיפוסים