הצגת המקור של הדף "בטיחות סוג"

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

אכיפת סוגים יכולה להיות סטטית, כלומר, לתפוס שגיאות פוטנציאליות בזמן הידור, או דינמית, כלומר לשייך מידע על הסוגים השונים לערכים בזמן ריצה ולהשתמש בסוגים הקיימים לפי הצורך כדי לזהות שגיאות קרובות, או שילוב של שתיהן.<ref>{{Cite web|title=What to know before debating type systems {{!}} Ovid [blogs.perl.org]|url=https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html|access-date=2023-06-27|website=blogs.perl.org}}</ref> אכיפה דינאמית מאפשרת לעיתים קרובות להפעיל תוכניות שיהיו לא חוקיות במסגרת אכיפה סטטית.

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

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

: תוכניות מוגדרות היטב מבחינת סוגים אינן יכולות "לעשות טעויות".<ref name="Milner 1978">{{Citation|last=Milner|first=Robin|title=A Theory of Type Polymorphism in Programming|journal=Journal of Computer and System Sciences|pages=348–375|volume=17|number=3|year=1978|doi=10.1016/0022-0000(78)90014-4}}</ref>

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

: שפה היא בטוחה מבחינת הסוגים שלה אם הפעולות היחידות שניתן לבצע בנתונים בשפה הן אלו המוגדרות לפי סוג המידע.<ref name="saraswat-java">{{Cite web|last=Saraswat|first=Vijay|date=1997-08-15|title=Java is not type-safe|url=http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html|access-date=2008-10-08}}</ref>

עם זאת, מה בדיוק המשמעות של תוכניות "מוגדרות היטב" או "עושות טעויות" זו מאפיין של הסמנטיקה ה[[שפת תכנות|סטטית]] והדינאמית של כל שפת תכנות. כתוצאה מכך, הגדרה מדויקת של תקינות כל סוג ספציפי תלויה בסגנון הסמנטיקה וההגדרות שכל שפת תכנות למה תקין ואינו תקין. בשנת 1994, אנדרו רייט ו[[מתיאס פלייזן]] ניסחו את מה שהפך להגדרה וטכניקת ההוכחה הסטנדרטית לבטיחות סוגים בשפות המוגדרות על ידי [[סמנטיקה תפעולית]],<ref name="Wright and Felleisen 1994">{{Cite journal|last=Wright|first=A. K.|last2=Felleisen|first2=M.|date=15 November 1994|title=A Syntactic Approach to Type Soundness|journal=Information and Computation|language=en|volume=115|issue=1|pages=38–94|doi=10.1006/inco.1994.1093|issn=0890-5401|doi-access=free}}</ref> שהיא הקרובה ביותר למושג בטיחות סוג כפי שרוב המתכנתים מבינים אותה. לפי גישה זו, הסמנטיקה של שפת תכנות חייבת להיות בעלת שני המאפיינים הבאים כדי להיחשב תקינה מבחינת טיפוסיות:

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

== קשר לצורות בטיחות אחרות ==
לבדה, תקינות טיפוס היא תכונה חלשה יחסית, שכן היא בעצם קובעת שהכללים של מערכת טיפוסים עקביים ואי אפשר לערער עליהם. עם זאת, בפועל, שפות תכנות מתוכננות כך שכתיבת קוד עם בטיחות סוג גבוהה טומנת בחובה גם תכונות אחרות וחזקות יותר, שחלקן כוללות:
* מניעת פעולות בלתי חוקיות. לדוגמה, מערכת טיפוס יכולה לדחות את הביטוי <code>3 / "Hello, World"</code> כלא חוקי, מכיוון [[אופרטור (תכנות)|שאופרטור]] החלוקה אינו מוגדר עבור [[מחלק]] [[מחרוזת (מדעי המחשב)|מחרוזת]].
* [[בטיחות זיכרון]]
** מערכות טיפוס יכולות למנוע מצבים שבהם מצביע בזיכרון מתייחס לאובייקס מהסוג הלא נכון.
** מערכות מסוגים מתוחכמות יותר, כגון אלו התומכות בסוגים תלויים, יכולות לזהות ולדחות גישה מחוץ לתחום, ולמנוע [[גלישת חוצץ]] פוטנציאלית.<ref>{{Cite book|last=Henriksen|first=Troels|title=Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming|last2=Elsman|first2=Martin|date=17 June 2021|publisher=Association for Computing Machinery|isbn=9781450384667|pages=1–14|chapter=Towards size-dependent types for array programming|doi=10.1145/3460944.3464310|chapter-url=https://dl.acm.org/doi/10.1145/3460944.3464310}}</ref>
* [[שגיאה לוגית|שגיאות לוגיות]] שמקורן ב[[סמנטיקה]] מסוגים שונים. לדוגמה, אינץ' ומילימטרים עשויים להיות מאוחסנים כמספרים שלמים, אך אין להחליף ביניהם. מערכת טיפוס יכולה לאכוף עבורם שני סוגים שונים של מספר שלם.

== שפות עם בטיחות סוג חזקה וחלשה ==
שפות תכנות מסווגות לרוב בבטיחות סוג חזקה או בטיחות סוג חלשה (שנקראת גם בבטיחות סוג רופפת) כאשר מתייחסים להיבטים מסוימים של בטיחות סוג. בשנת 1974, [[ברברה ליסקוב|ליסקוב]] וזילס הגדירו שפה עם בטיחות סוג חזקה ככזו שבה "בכל פעם שאובייקט מועבר מפונקציה קוראת לפונקציה שנקראת, הסוג שלו חייב להיות תואם לסוג שהוכרז בפונקציה הנקראת".<ref>{{Cite journal|last=Liskov|first=B|last2=Zilles|first2=S|year=1974|title=Programming with abstract data types|journal=ACM SIGPLAN Notices|volume=9|issue=4|pages=50–59|citeseerx=10.1.1.136.3043|doi=10.1145/942572.807045}}</ref> בשנת 1977, כתב ג'קסון, "בשפה עם בטיחות סוג חזקה לכל שדה נתונים יהיה סוג נפרד וכל תהליך יציין את דרישות התקשורת שלו במונחים של סוגים אלה."<ref>{{Cite book|last=Jackson|first=K.|title=Design and Implementation of Programming Languages|year=1977|isbn=3-540-08360-X|series=Lecture Notes in Computer Science|volume=54|pages=436–443|chapter=Parallel processing and modular software construction|doi=10.1007/BFb0021435}}</ref> לעומת זאת, שפה עם בטיחות סוג חלשה עשויה להניב תוצאות בלתי צפויות או לבצע המרת סוג מרומזת (כלומר שההמרה תתבצע ללא הצהרה מכוונת של כותב הקוד שהוא מתכוון לשנות את סוג האובייקט).<ref>{{Cite web|date=2005|title=CS1130. Transition to OO programming. – Spring 2012 --self-paced version|url=https://www.cs.cornell.edu/courses/cs1130/2012sp/1130selfpaced/module1/module1part4/strongtyping.html|access-date=2023-09-15|publisher=Cornell University, Department of Computer Science}}</ref>

== ניהול זיכרון ובטיחות סוג ==
בטיחות סוג קשורה קשר הדוק לבטיחות זיכרון. כך למשל, ביישום של שפה שיש לה סוג כלשהו בשם <math>t</math> המאפשר דפוסי סיביות מסוימים אך לא אחרים, שגיאת זיכרון מסוג מצביע תועה מאפשרת כתיבת תבנית סיביות שאינה מייצגת ייצוג לגיטימי של <math>t</math> לתוך [[משתנה (תכנות)|משתנה]] מת מסוג <math>t</math>, מה שגורם לשגיאת סוג כאשר המשתנה נקרא. לעומת זאת, אם השפה בטוחה מבחינת ניהול זיכרון, היא לא יכולה לאפשר שימוש במספר שלם שרירותי כ[[מצביע]], ולכן חייב להיות סוג מיוחד עבור מצביעים והפניות שרירותיות.

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

רוב השפות המתאפיינות בבטיחות סוג חזקה משתמשות ב[[איסוף זבל (מדעי המחשב)|איסוף זבל]]. פירס אומר, "קשה מאוד להשיג בטיחות סוג בנוכחות פעולת deallocation מפורשת", עקב בעיית המצביע התועה.<ref>{{Cite book|last=Pierce|first=Benjamin C.|title=Types and programming languages|date=2002|publisher=MIT Press|isbn=0-262-16209-1|location=Cambridge, Mass.|page=158}}</ref> עם זאת, [[ראסט (שפת תכנות)|ראסט]] נחשבת באופן כללי לשפה שמתאפיינת בבטיחות סוג חזקה ומשתמשת באלגוריתם הבודק כל השאלה של משתנה כדי להשיג בטיחות זיכרון, במקום איסוף אשפה.

== בטיחות סוג בשפות מונחות עצמים ==
בשפות [[תכנות מונחה-עצמים|מונחות עצמים]] בטיחות סוג בדרך כלל מובנית ב[[מערכת טיפוסים|מערכת הטיפוסים]] של השפה. תכונה זו מתבטאת בהגדרת ה[[מחלקה (תכנות)|מחלקות]].

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

כל פונקציה המחליפה אובייקטים שמקורם במחלקה מסוימת, או מיישמת [[ממשק (תכנות)|ממשק]] ספציפי, תעמוד בחוזה הזה: מכאן שבפונקציה זו הפעולות המותרות על אותו אובייקט יהיו רק אלו המוגדרות בשיטות של המחלקה שהאובייקט מיישם. זה יבטיח כי שלמות האובייקט תישמר.<ref>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 itegrity</ref>

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

== ראו גם ==
* [[מערכת טיפוסים]]

== הערות שוליים ==
{{הערות שוליים}}

[[קטגוריה:מדעי המחשב]]