أمان النوع

في علوم الحاسوب ، يُقصد بأمان النوع مدى قدرة لغة البرمجة على الحد من أخطاء النوع أو منعها . وتُسمى اللغات الآمنة من حيث النوع أحيانًا باللغات ذات النوع القوي أو الصارم . أما السلوكيات التي تُصنف على أنها أخطاء نوع في لغة برمجة معينة، فهي عادةً تلك الناتجة عن محاولات إجراء عمليات على قيم ليست من نوع البيانات المناسب ، مثل محاولة جمع سلسلة نصية مع عدد صحيح .

يمكن أن يكون فرض أنواع البيانات ثابتًا (أي اكتشاف الأخطاء المحتملة أثناء الترجمة )، أو ديناميكيًا (أي ربط معلومات النوع بالقيم أثناء التشغيل والرجوع إليها عند الحاجة لاكتشاف الأخطاء الوشيكة)، أو مزيجًا من الاثنين. ^{[ 1 ]} غالبًا ما يسمح فرض أنواع البيانات الديناميكي بتشغيل برامج غير صالحة في ظل الفرض الثابت، ولكن على حساب إدخال أخطاء أثناء التشغيل.

في سياق أنظمة الأنواع الثابتة (التي تُترجم في وقت الترجمة)، تتضمن سلامة النوع عادةً (من بين أمور أخرى) ضمان أن القيمة النهائية لأي تعبير ستكون عضوًا شرعيًا في نوعه الثابت. لكن الشرط الدقيق أكثر تعقيدًا من ذلك - انظر، على سبيل المثال، إلى التنميط الفرعي وتعدد الأشكال لمزيد من التفاصيل.

بشكل بديهي، يمكن تلخيص سلامة النوع في عبارة روبن ميلنر الموجزة التي تقول

البرامج المكتوبة بشكل جيد لا يمكن أن "تخطئ". ^{[ 2 ]}

بمعنى آخر، إذا كان نظام الأنواع سليمًا ، فإن التعبيرات التي يقبلها هذا النظام يجب أن تُقيّم إلى قيمة من النوع المناسب (بدلاً من إنتاج قيمة من نوع آخر غير ذي صلة أو التسبب في خطأ في النوع). يقدم فيجاي ساراسوات التعريف التالي ذي الصلة:

تكون اللغة آمنة من حيث النوع إذا كانت العمليات الوحيدة التي يمكن إجراؤها على البيانات في اللغة هي تلك المسموح بها من قبل نوع البيانات. ^{[ 3 ]}

مع ذلك، فإنّ ما يعنيه تحديدًا أن يكون البرنامج "مُصنَّفًا بشكل صحيح" أو أن "يحدث به خلل" يعتمد على خصائص دلالاته الثابتة والديناميكية ، وهي خصائص خاصة بكل لغة برمجة. وبالتالي، فإنّ التعريف الرسمي الدقيق لسلامة النوع يعتمد على أسلوب الدلالات الرسمية المُستخدمة لتحديد اللغة. في عام ١٩٩٤، صاغ أندرو رايت وماتياس فيليسين ما أصبح التعريف القياسي وتقنية إثبات سلامة النوع في اللغات المُعرَّفة بدلالات تشغيلية ، ^{[ ٤ ]} وهو الأقرب إلى مفهوم سلامة النوع كما يفهمه معظم المبرمجين. وفقًا لهذا النهج، يجب أن تتوافر في دلالات اللغة الخاصيتان التاليتان لتُعتبر سليمة النوع:

تقدم

البرنامج المصمم بشكل صحيح لا يعلق أبدًا: فكل تعبير إما أن يكون قيمةً بالفعل أو يمكن اختزاله إلى قيمة بطريقة محددة جيدًا. بعبارة أخرى، لا يصل البرنامج أبدًا إلى حالة غير محددة حيث لا يمكن إجراء أي انتقالات أخرى.

الحفظ (أو تقليص الموضوع )

بعد كل خطوة تقييم، يظل نوع كل تعبير كما هو (أي يتم الحفاظ على نوعه ).

كما نُشر عدد من المعالجات الرسمية الأخرى لسلامة النوع من حيث الدلالات الدلالية والدلالات التشغيلية البنيوية . ^{[ 2 ] [ 5 ] [ 6 ]}

بمعزل عن السياق، تُعدّ سلامة النوع خاصية ضعيفة نسبيًا، إذ إنها ببساطة تنص على أن قواعد نظام النوع متسقة داخليًا ولا يمكن تجاوزها. مع ذلك، في الواقع العملي، تُصمّم لغات البرمجة بحيث تتضمن سلامة النوع أيضًا خصائص أخرى أقوى، منها:

• منع العمليات غير القانونية. على سبيل المثال، يمكن لنظام النوع رفض التعبير باعتباره غير صالح، لأن عامل3 / "Hello, World" القسمة غير مُعرَّف لمقسوم السلسلة .
• سلامة الذاكرة
  • يمكن لأنظمة الأنواع أن تمنع المؤشرات الجامحة التي قد تنشأ لولا ذلك من معاملة مؤشر إلى نوع واحد من الكائنات كمؤشر إلى نوع آخر.
  • يمكن لأنظمة الأنواع الأكثر تطوراً، مثل تلك التي تدعم الأنواع التابعة ، اكتشاف عمليات الوصول خارج النطاق ورفضها، مما يمنع حدوث تجاوزات محتملة في المخزن المؤقت . ^{[ 7 ]}
• تنشأ الأخطاء المنطقية من اختلاف دلالات الأنواع المختلفة. على سبيل المثال، يمكن تخزين البوصات والمليمترات كأعداد صحيحة، ولكن لا يجوز استبدال أحدهما بالآخر أو جمعهما. يمكن لنظام الأنواع فرض نوعين مختلفين من الأعداد الصحيحة لهما.

عادةً ما يُعدّ أمان النوع شرطًا أساسيًا لأي لغة برمجة تجريبية (أي لغة متخصصة ) تُقترح في أبحاث لغات البرمجة الأكاديمية. مع ذلك، فإن العديد من اللغات أكبر من أن تُبرهن عليها البشر يدويًا، إذ غالبًا ما تتطلب فحص آلاف الحالات. ومع ذلك، فقد ثبت أن بعض اللغات، مثل Standard ML ، التي تتميز بدلالات محددة بدقة، تُلبي أحد تعريفات أمان النوع. ^{[ 8 ]} ويُعتقد أن بعض اللغات الأخرى، مثل Haskell، تُلبي تعريفًا ما لأمان النوع، شريطة عدم استخدام بعض ميزات "الهروب" (على سبيل المثال، دالة unsafePerformIO في Haskell ، المستخدمة "للهروب" من البيئة المقيدة المعتادة التي تسمح بالإدخال/الإخراج ، تتجاوز نظام النوع، وبالتالي يمكن استخدامها لخرق أمان النوع. ^{[ 9 ]} ). يُعدّ التلاعب بالأنواع مثالًا آخر على ميزة "الهروب" هذه. بغض النظر عن خصائص تعريف اللغة، قد تحدث بعض الأخطاء أثناء التشغيل بسبب أخطاء في التنفيذ، أو في المكتبات المرتبطة المكتوبة بلغات أخرى؛ وقد تجعل هذه الأخطاء نوع تنفيذ معين غير آمن في ظروف معينة. كانت إحدى النسخ المبكرة من آلة جافا الافتراضية من صن عرضة لهذا النوع من المشاكل. ^{[ 3 ]}

غالبًا ما تُصنَّف لغات البرمجة، بشكلٍ عام، إلى لغات ذات أنواع بيانات قوية أو لغات ذات أنواع بيانات ضعيفة (أو ذات أنواع بيانات غير دقيقة) للإشارة إلى جوانب معينة من سلامة أنواع البيانات. في عام 1974، عرّف ليسكوف وزيلز اللغة ذات أنواع البيانات القوية بأنها اللغة التي "عند تمرير أي كائن من دالة مُستدعِية إلى دالة مُستدعاة، يجب أن يكون نوعه متوافقًا مع النوع المُعلن عنه في الدالة المُستدعاة". ^{[ 10 ]} وفي عام 1977، كتب جاكسون: "في اللغة ذات أنواع البيانات القوية، يكون لكل منطقة بيانات نوع بيانات مميز، وتُحدد كل عملية متطلبات الاتصال الخاصة بها بدلالة هذه الأنواع". ^{[ 11 ]} في المقابل، قد تُنتج اللغة ذات أنواع البيانات الضعيفة نتائج غير متوقعة أو قد تُجري تحويلًا ضمنيًا لأنواع البيانات. ^{[ 12 ]}

يرتبط أمان النوع ارتباطًا وثيقًا بأمان الذاكرة . على سبيل المثال، في تطبيق لغة تحتوي على نوع معين${\displaystyle t}$يسمح هذا ببعض أنماط البتات دون غيرها، ويسمح خطأ في ذاكرة المؤشر المعلق بكتابة نمط بتات لا يمثل عضوًا شرعيًا من${\displaystyle t}$إلى متغير ميت من النوع${\displaystyle t}$مما يتسبب في حدوث خطأ في النوع عند قراءة المتغير. وعلى العكس من ذلك، إذا كانت اللغة آمنة من حيث الذاكرة، فلا يمكنها السماح باستخدام عدد صحيح عشوائي كمؤشر ، وبالتالي يجب أن يكون هناك نوع مؤشر أو مرجع منفصل.

كشرط أساسي، يجب ألا تسمح لغة البرمجة الآمنة من حيث النوع بوجود مؤشرات معلقة بين تخصيصات من أنواع مختلفة. لكن معظم اللغات تفرض الاستخدام الصحيح لأنواع البيانات المجردة التي يُعرّفها المبرمجون، حتى عندما لا يكون ذلك ضروريًا تمامًا لسلامة الذاكرة أو لمنع أي نوع من الأعطال الكارثية. تُعطى التخصيصات نوعًا يصف محتوياتها، ويظل هذا النوع ثابتًا طوال مدة التخصيص. وهذا يسمح لتحليل الأسماء المستعارة القائم على النوع باستنتاج أن التخصيصات من أنواع مختلفة متميزة.

تستخدم معظم لغات البرمجة الآمنة من حيث النوع آلية جمع البيانات المهملة . يقول بيرس: "من الصعب للغاية تحقيق أمان النوع في وجود عملية تحرير صريحة للذاكرة"، وذلك بسبب مشكلة المؤشر المعلق. ^{[ 13 ]} ومع ذلك، تُعتبر لغة Rust آمنة من حيث النوع بشكل عام، وتستخدم مدقق الاستعارة لتحقيق أمان الذاكرة، بدلاً من جمع البيانات المهملة.

في لغات البرمجة الكائنية التوجه، عادةً ما يكون أمان النوع متأصلاً في وجود نظام أنواع . ويتم التعبير عن ذلك من خلال تعريفات الفئات.

يُعرّف الصنف أساسًا بنية الكائنات المشتقة منه، وتُعرّف واجهة برمجة التطبيقات (API) بمثابة عقد للتعامل مع هذه الكائنات. في كل مرة يتم فيها إنشاء كائن جديد، فإنه يلتزم بهذا العقد.

كل دالة تتبادل كائنات مشتقة من فئة معينة، أو تُنفذ واجهة معينة ، ستلتزم بهذا العقد: وبالتالي، فإن العمليات المسموح بها في تلك الدالة على ذلك الكائن ستكون فقط تلك المُعرَّفة بواسطة أساليب الفئة التي يُنفذها الكائن. وهذا سيضمن الحفاظ على سلامة الكائن. ^{[ 14 ]}

الاستثناءات من ذلك هي لغات البرمجة الكائنية التي تسمح بالتعديل الديناميكي لبنية الكائن، أو استخدام الانعكاس لتعديل محتوى الكائن للتغلب على القيود التي تفرضها تعريفات أساليب الفئة.

توضح الأمثلة التالية كيف يمكن لمعاملات التحويل في لغة C++ أن تُخلّ بسلامة النوع عند استخدامها بشكل خاطئ. يُظهر المثال الأول كيف يمكن تحويل أنواع البيانات الأساسية بشكل خاطئ:

#include <iostream> using namespace std ;int main () { int ival = 5 ; // قيمة عددية صحيحة float fval = reinterpret_cast < float &> ( ival ); // إعادة تفسير نمط البت cout << fval << endl ; // إخراج العدد الصحيح كعدد عشري return 0 ; }

في هذا المثال، reinterpret_castيمنع هذا صراحةً المُصرّف من إجراء تحويل آمن من عدد صحيح إلى قيمة عشرية. ^{[ 21 ]} عند تشغيل البرنامج، سيُخرج قيمة عشرية غير صالحة. كان من الممكن تجنب هذه المشكلة بكتابة الكود التالي بدلاً من ذلك.float fval = ival;

يوضح المثال التالي كيف يمكن تحويل مراجع الكائنات إلى نوع فرعي بشكل غير صحيح:

#include <iostream> using namespace std ;class Parent { public : virtual ~ Parent () {} // مُدمِّر افتراضي لـ RTTI };class Child1 : public Parent { public : int a ; };class Child2 : public Parent { public : float b ; };int main () { Child1 c1 ; c1 . a = 5 ; Parent & p = c1 ; // التحويل التصاعدي آمن دائمًا Child2 & c2 = static_cast < Child2 &> ( p ); // تحويل تنازلي غير صالح cout << c2 . b << endl ; // سيُخرج بيانات غير صالحة return 0 ; }

تحتوي الفئتان الفرعيتان على أعضاء من أنواع مختلفة. عند تحويل مؤشر من الفئة الأصلية إلى مؤشر من الفئة الفرعية، قد لا يشير المؤشر الناتج إلى كائن صالح من النوع الصحيح. في المثال، يؤدي هذا إلى طباعة قيمة غير صالحة. كان من الممكن تجنب هذه المشكلة باستبدالها static_castبـ dynamic_cast`include` التي تُطلق استثناءً عند التحويلات غير الصالحة. ^{[ 22 ]}

• نظرية الأنواع

• بيرس، بنجامين سي. (2002). أنواع لغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا. ISBN 978-0-262-16209-8.
• "Type Safe" . ويكي مستودع أنماط بورتلاند .
• رايت، أندرو ك.؛ ماتياس فيليسين (1994). "مقاربة نحوية لسلامة النوع" . المعلومات والحوسبة . 115 (1): 38-94 . doi : 10.1006/inco.1994.1093 .
• ماكراكيس، ستافروس (أبريل 1982). "الأمان والطاقة". ملاحظات هندسة البرمجيات ACM SIGSOFT . 7 (2): 25-26 . doi : 10.1145/1005937.1005941 . S2CID 10426644 .