בטיחות טיפוס
במדעי המחשב, בטיחות טיפוס ותקינות טיפוס הן המידה שבה שפת תכנות מרתיעה או מונעת שגיאות טיפוס. שפות תכנות שונות מגדירות איך לטפל בסתירות או בעיות בהגדרות הטיפוסים בשפה. כאשר נתקלים בבעיה שכזו, היא תוכל לגרור למשל שגיאה, אזהרה או פשוט התעלמות מהבעיה. ההתנהגויות המסווגות כשגיאות טיפוס על ידי שפות תכנות שונות נובעות בדרך כלל מניסיונות לבצע פעולות על ערכים שאינם מהטיפוס המתאים. למשל, הוספת מחרוזת למספר שלם כאשר אין הגדרה כיצד לטפל במקרה זה. שפות תכנות שונות מגדירות תחביר שונה, וביטוי או פעולה שמותרת בשפת תכנות מסוימת עלולה לגרום לשגיאת טיפוס בשפה אחרת.
אכיפת טיפוסים יכולה להיות סטטית, כלומר, לתפוס שגיאות פוטנציאליות בזמן הידור, או דינמית, כלומר לשייך מידע על הטיפוסים השונים לערכים בזמן ריצה ולהשתמש בטיפוסים הקיימים לפי הצורך כדי לזהות שגיאות קרובות, או שילוב של שתיהן.[1] אכיפה דינאמית מאפשרת לעיתים קרובות להפעיל תוכניות שיהיו לא חוקיות במסגרת אכיפה סטטית.
בהקשר של מערכות סטטיות (זמן הידור), בטיחות טיפוס כרוכה בדרך כלל (בין היתר) בהבטחה שהערך הסופי של כל ביטוי יהיה לגיטימי בטיפוס הסטטי של אותו ביטוי. הדרישה המדויקת היא מורכבת יותר מכך, למשל, במקרים שבהם השפה תומכת בתת-טיפוסים ופולימורפיזם.
הגדרות
[עריכת קוד מקור | עריכה]תקינות טיפוס מתארת את מידת ההגנה של שפת תכנות מפני שגיאות טיפוס. לפי רובין מילנר, "תוכניות שמוגדרות היטב מבחינת טיפוסים אינן יכולות לבצע שגיאות"[2]. המשמעות היא שאם מערכת הטיפוסים עקבית, ביטויים בשפה יישארו בטיפוס המתאים ולא יגרמו לשגיאות בזמן ריצה. אם הפעולות היחידות שניתן לבצע בנתונים בשפה הן אלו המוגדרות לפי טיפוס המידע[3]. ההגדרה הפורמלית של תקינות משתנה בהתאם לסמנטיקה של השפה. לפי ההגדרה המקובלת (Wright ו־Felleisen, 1994), שפה נחשבת תקינה טיפוסית אם מתקיימים בה שני תנאים:
שילוב שני התנאים מבטיח שהתוכנית לא "תיתקע" ולא תסטה מהגדרות הטיפוס שלה.
עם זאת, מה בדיוק המשמעות של תוכניות "מוגדרות היטב" או "עושות טעויות" זו מאפיין של הסמנטיקה הסטטית והדינאמית של כל שפת תכנות. כתוצאה מכך, הגדרה מדויקת של תקינות כל טיפוס ספציפי תלויה בסגנון הסמנטיקה וההגדרות שכל שפת תכנות מעניקה למה שתקין ואינו תקין. בשנת 1994, אנדרו רייט ומתיאס פלייזן ניסחו את מה שהפך להגדרה וטכניקת ההוכחה הסטנדרטית לבטיחות טיפוסים בשפות המוגדרות על ידי סמנטיקה תפעולית, שהיא הקרובה ביותר למושג בטיחות טיפוס כפי שרוב המתכנתים מבינים אותה.
המשמעות של תוכניות "מוגדרות היטב" תלויה בסמנטיקה הסטטית והדינאמית של שפת התכנות. לכן, ההגדרה המדויקת של תקינות טיפוס משתנה בין שפות שונות בהתאם לסגנון הסמנטי שלהן. בשנת 1994, אנדרו רייט ומתיאס פלייזן הציעו הגדרה וטכניקת הוכחה שנחשבת מאז לסטנדרט לבטיחות טיפוסים בשפות בעלות סמנטיקה תפעולית[4] – שהיא גם הקרובה ביותר להבנה המקובלת של מתכנתים למושג זה.
קשר לצורות בטיחות אחרות
[עריכת קוד מקור | עריכה]לבדה, תקינות טיפוס היא תכונה חלשה יחסית, שכן היא בעצם קובעת שהכללים של מערכת טיפוסים עקביים ואי אפשר לערער עליהם. עם זאת, בפועל, שפות תכנות מתוכננות כך שכתיבת קוד עם בטיחות טיפוס גבוהה טומנת בחובה גם תכונות אחרות וחזקות יותר, שחלקן כוללות:
- מניעת פעולות בלתי חוקיות. לדוגמה, מערכת טיפוסים יכולה לדחות את הביטוי
3 / "Hello, World"כלא חוקי, מכיוון שאופרטור החלוקה אינו מוגדר עבור מחלק מחרוזת.
- בטיחות זיכרון
- מערכות טיפוסים יכולות למנוע מצבים שבהם מצביע בזיכרון מתייחס לאובייקט מהטיפוס הלא נכון.
- מערכות טיפוסים מתוחכמות יותר, כגון אלו התומכות בטיפוסים תלויים, יכולות לזהות ולדחות גישה מחוץ לתחום, ולמנוע גלישת חוצץ פוטנציאלית.[5]
שגיאות לוגיות שמקורן בסמנטיקה של טיפוסים שונים. לדוגמה, אינץ' ומילימטרים עשויים להיות מאוחסנים כמספרים שלמים, אך אין להחליף ביניהם. מערכת טיפוסים יכולה לאכוף עבורם שני טיפוסים שונים של מספר שלם.
שפות עם בטיחות טיפוס חזקה וחלשה
[עריכת קוד מקור | עריכה]שפות תכנות מסווגות לרוב כבעלות בטיחות טיפוס חזקה או בטיחות טיפוס חלשה (שנקראת גם בטיחות טיפוס רופפת) כאשר מתייחסים להיבטים מסוימים של בטיחות טיפוס. בשנת 1974, ליסקוב וזילס הגדירו שפה עם בטיחות טיפוס חזקה ככזו שבה "בכל פעם שאובייקט מועבר מפונקציה קוראת לפונקציה שנקראת, הטיפוס שלו חייב להיות תואם לטיפוס שהוכרז בפונקציה הנקראת."[6] בשנת 1977, כתב ג'קסון, "בשפה עם בטיחות טיפוס חזקה לכל שדה נתונים יהיה טיפוס נפרד וכל תהליך יציין את דרישות התקשורת שלו במונחים של טיפוסים אלה."[7] לעומת זאת, שפה עם בטיחות טיפוס חלשה עשויה להניב תוצאות בלתי צפויות או לבצע המרת טיפוס מרומזת (כלומר שההמרה תתבצע ללא הצהרה מכוונת של כותב הקוד שהוא מתכוון לשנות את טיפוס האובייקט).[8]
ניהול זיכרון ובטיחות טיפוס
[עריכת קוד מקור | עריכה]בטיחות טיפוס קשורה קשר הדוק לבטיחות זיכרון. כך למשל, ביישום של שפה שיש לה טיפוס כלשהו בשם המאפשר דפוסי סיביות מסוימים אך לא אחרים, שגיאת זיכרון מסוג מצביע תועה מאפשרת כתיבת תבנית סיביות שאינה מייצגת ייצוג לגיטימי של לתוך משתנה מטיפוס , מה שגורם לשגיאת טיפוס כאשר המשתנה נקרא. לעומת זאת, אם השפה בטוחה מבחינת ניהול זיכרון, היא לא יכולה לאפשר שימוש במספר שלם שרירותי כמצביע, ולכן חייב להיות טיפוס מיוחד עבור מצביעים והפניות שרירותיות.
כתנאי מינימלי, שפה שמאופיינת בבטיחות טיפוס גבוהה, לא מאפשרת מצביעים תועים בהקצאות מטיפוסים שונים, אבל רוב השפות אוכפות שימוש נכון בטיפוסי נתונים מופשטים שהוגדרו על ידי מתכנתים גם כאשר הדבר אינו הכרחי לבטיחות הזיכרון או למניעת כשל קטסטרופלי. כל אובייקט שמוקצה מקבל טיפוס המתאר את תוכנו, וטיפוס זה קבוע למשך ההקצאה. דבר זה מאפשר לניתוח כינוי מבוסס טיפוסים להסיק שהקצאות מטיפוסים שונים הן שונות.
רוב השפות המתאפיינות בבטיחות טיפוס חזקה משתמשות באיסוף זבל. פירס אומר, "קשה מאוד להשיג בטיחות טיפוס בנוכחות פעולת deallocation מפורשת", עקב בעיית המצביע התועה.[9] עם זאת, ראסט נחשבת באופן כללי לשפה שמתאפיינת בבטיחות טיפוס חזקה ומשתמשת באלגוריתם הבודק כל השאלה של משתנה כדי להשיג בטיחות זיכרון, במקום איסוף אשפה.
בטיחות טיפוס בשפות מונחות עצמים
[עריכת קוד מקור | עריכה]בשפות מונחות עצמים בטיחות טיפוס בדרך כלל מובנית במערכת הטיפוסים של השפה. תכונה זו מתבטאת בהגדרת המחלקות.
מחלקה מגדירה את מבנה האובייקטים הנגזרים ממנה ואת ממשק API כ"חוזה" לשימוש באובייקטים אלו. בכל פעם שנוצר אובייקט חדש הוא "יעמוד" בחוזה זה.
כל פונקציה המחליפה אובייקטים שמקורם במחלקה מסוימת, או מיישמת ממשק ספציפי, תעמוד בחוזה הזה: מכאן שבפונקציה זו הפעולות המותרות על אותו אובייקט יהיו רק אלו המוגדרות בשיטות של המחלקה שהאובייקט מיישם. זה יבטיח כי שלמות האובייקט תישמר.[10]
חריגות לכך הן שפות מונחות עצמים המאפשרות שינוי דינמי של מבנה האובייקט, או שימוש ברפלקציה כדי לשנות את התוכן של אובייקט ולהתגבר על האילוצים המוטלים על ידי מבנה המחלקה.
הערות שוליים
[עריכת קוד מקור | עריכה]- ^ "What to know before debating type systems | Ovid [blogs.perl.org]". blogs.perl.org. נבדק ב-2023-06-27.
- ^ Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences, 17 (3): 348–375, doi:10.1016/0022-0000(78)90014-4
- ^ Saraswat, Vijay (1997-08-15). "Java is not type-safe". נבדק ב-2008-10-08.
- ^ Wright, A. K.; Felleisen, M. (15 בנובמבר 1994). "A Syntactic Approach to Type Soundness". Information and Computation (באנגלית). 115 (1): 38–94. doi:10.1006/inco.1994.1093. ISSN 0890-5401.
{{cite journal}}: (עזרה) - ^ Henriksen, Troels; Elsman, Martin (17 ביוני 2021). "Towards size-dependent types for array programming". Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming. Association for Computing Machinery. pp. 1–14. doi:10.1145/3460944.3464310. ISBN 9781450384667.
{{cite book}}: (עזרה) - ^ Liskov, B; Zilles, S (1974). "Programming with abstract data types". ACM SIGPLAN Notices. 9 (4): 50–59. CiteSeerX 10.1.1.136.3043. doi:10.1145/942572.807045.
- ^ Jackson, K. (1977). "Parallel processing and modular software construction". Design and Implementation of Programming Languages. Lecture Notes in Computer Science. Vol. 54. pp. 436–443. doi:10.1007/BFb0021435. ISBN 3-540-08360-X.
- ^ "CS1130. Transition to OO programming. – Spring 2012 --self-paced version". Cornell University, Department of Computer Science. 2005. נבדק ב-2023-09-15.
- ^ Pierce, Benjamin C. (2002). Types and programming languages. Cambridge, Mass.: MIT Press. p. 158. ISBN 0-262-16209-1.
- ^ Type safety is hence also a matter of good class definition: public methods that modify the internal state of an object shall preserve the object integrity