Predicate Subtypes in VerCors
تقدم هذه الورقة تنفيذًا أوليًا في برنامج التحقق VerCors يدعم الأنواع الفرعية للمحمولات (predicate subtypes) لتحديد قيود نطاق المتغيرات، ويتميز بالتوليد التلقائي للمواصفات، والقدرة على دمج أنواع فرعية متعددة، ووضع التشغيل الصارم لتعزيز فحص تجاوز السعة.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تبني بيتاً من ورق اللعب. في عالم برمجة الكمبيوتر، "أوراق اللعب" هي المتغيرات (مثل الأرقام أو القوائم)، و"البيت" هو البرنامج. عادةً، عندما تعلن عن متغير، فأنت تقول فقط: "هذا رقم". ولكن في الواقع، ليس أي رقم سيفي بالغرض. فربما تحتاج إلى رقم لا يمكن أن يكون صفراً أبداً (حتى لا تقسم عليه)، أو رقماً يتسع داخل صندوق صغير (حتى لا يكسر النظام).
تقدم هذه الورقة ميزة جديدة لأداة تسمى VerCors، وهي تشبه المفتش الذكي للغاية الذي يتحقق مما إذا كان بيت الورق الخاص بك سيصمد قبل أن تبدأ في بنائه حتى. الميزة الجديدة تسمى الأنواع الفرعية التقريرية (Predicate Subtypes).
إليك تفصيل كيفية عمل ذلك، باستخدام بعض التشبيهات من الحياة اليومية:
1. المشكلة: خطأ "أي رقم"
تخيل أنك تخبر عامل بناء: "أحضر لي طوبة". قد يحضر لك صخرة ضخمة، أو حصاة صغيرة، أو طوبة حقيقية. إذا كان جدارك يحتاج إلى حجم محدد، فإن الصخرة ستؤدي إلى انهيار الهيكل بالكامل.
في البرمجة، إذا قلت للكمبيوتر: "هذا المتغير هو عدد صحيح (integer)"، يفترض الكمبيوتر أنه يمكن أن يكون أي عدد صحيح، من سالب ما لا نهاية إلى موجب ما لا نهاية. ولكن في العالم الحقيقي (وفي برامج معينة)، غالباً ما نحتاج إلى قول: "هذا العدد الصحيح يجب أن يكون بين 0 و100"، أو "هذا العدد الصحيح يجب ألا يكون صفراً أبداً".
بدون هذه الميزة، قد يغفل الكمبيوتر عن خطأ حيث يصبح الرقم كبيراً جداً (تجاوز السعة/overflow) أو يصبح صفراً عندما لا ينبغي له ذلك، مما يؤدي إلى تعطل البرنامج لاحقاً.
2. الحل: "الملصق الخاص" (الأنواع الفرعية التقريرية)
أضاف المؤلفون طريقة لوضع ملصق خاص على متغيراتك. بدلاً من مجرد قول "هذا رقم"، يمكنك قول:
- "هذا رقم غير صفري".
- "هذا رقم قصير (بين -128 و127)".
- "هذا فهرس صالح (رقم يتناسب داخل هذه القائمة المحددة)".
في الورقة البحثية، يسمون هذه الأنواع الفرعية التقريرية (Predicate Subtypes). فكر في الأمر كأنه بطاقة دخول لكبار الشخصيات (VIP). إذا كان للمتغير بطاقة "غير صفري"، فإن الكمبيوتر يعرف أنه يُمنع منعاً باتاً أن يكون صفراً.
3. كيف يعمل المفتش (الفحوصات التلقائية)
الجزء الأكثر روعة في هذه الورقة هو أن أداة VerCors تقوم بالعمل الشاق تلقائياً. لست بحاجة إلى كتابة مئات الفحوصات المختلفة للتأكد من أن أرقامك آمنة.
- المترجم السحري: عندما تكتب
int xمع ملصق "غير صفري"، تعمل VerCors كمترجم؛ فهي تعيد كتابة الكود الخاص بك سراً في الخلفية لإضافة فحوصات السلامة. - الحارس عند الباب: في كل مرة تحاول فيها وضع قيمة جديدة في هذا المتغير، تضع VerCors حارساً عند الباب. يتحقق الحارس: "هل القيمة الجديدة تحقق شرط الملصق؟"
- إذا حاولت وضع
0في متغير "غير صفري"، سيوقفك الحارس ويقول: "خطأ! هذا لا يطابق الملصق". - إذا حاولت وضع
5، سيقول الحارس: "كل شيء آمن!".
- إذا حاولت وضع
4. "الوضع الصارم": فحص الرحلة، وليس الوجهة فقط
هذا هو الجزء الأكثر ذكاءً في الورقة. أحياناً، تكون النتيجة النهائية سليمة، لكن الرحلة للوصول إليها كانت خطيرة.
التشبيه: تخيل أنك تقود سيارة يمكنها حمل 100 رطل من البضائع فقط.
- الوضع العادي: تقوم بتحميل 50 رطلاً، ثم تمر فوق جسر ينهار تحت وزن 200 رطل، ثم تفرغ 50 رطلاً. الوزن النهائي هو 50 (آمن)، لكنك حطمت الجسر في الطريق!
- الوضع الصارم: السيارة تحمل ملصق "صارم". هذا يعني أن كل خطوة في الرحلة يجب أن تظل تحت 100 رطل. حتى لو كنت تقوم بعملية حسابية سريعة في منتصف الطريق، فإن الكمبيوتر يتحقق مما إذا كان هذا الرقم المؤقت آمناً.
تقدم الورقة وضع "الحساب الصارم" (Strict Arithmetic). إذا قمت بتفعيله، فإن VerCors تتحقق من كل عملية حسابية صغيرة (مثل x - 2) للتأكد من أنها لا تتسبب مؤقتاً في انفجار حجم الرقم (تجاوز السعة)، حتى لو كانت النتيجة النهائية آمنة. هذا أمر بالغ الأهمية لمنع "تجاوز السعة" (عندما يصبح الرقم كبيراً جداً بحيث لا يستطيع الكمبيوتر التعامل معه).
5. خلط وتوفيق الملصقات
تماماً كما يمكنك ارتداء قبعة ووشاح في نفس الوقت، يمكنك دمج هذه الملصقات.
- يمكنك القول إن المتغير يجب أن يكون غير صفري وَ موجباً.
- يمكنك القول إنه يجب أن يكون إما رقماً قصيراً أَوْ رقماً طويلاً.
- يمكنك حتى القول "إذا لم يكن فارغاً (Null)، فيجب أن يكون طوله 3".
تتعامل الأداة مع كل هذه التوليفات المعقدة تلقائياً، وتحولها إلى فحوصات سلامة بسيطة يمكن للكمبيوتر فهمها.
لماذا يهم هذا؟
في الماضي، كان على المبرمجين كتابة فحوصات السلامة يدوياً في كل مكان، وهو أمر ممل وسهل الخطأ. أو كان عليهم استخدام أنظمة جامدة للغاية لا يمكنها التعامل مع القواعد المعقدة.
تظهر هذه الورقة أن VerCors يمكنها الآن:
- فهم القواعد المعقدة حول بياناتك (مثل "هذه القائمة يجب أن تحتوي على 3 عناصر بالضبط").
- التحقق تلقائياً من أن تلك القواعد لا تُكسر أبداً، حتى في منتصف عملية حسابية.
- رصد حالات تجاوز السعة الخطيرة قبل أن يعمل البرنامج فعلياً، مما يوفر الوقت ويمنع الانهيارات.
ملخص
فكر في الأنواع الفرعية التقريرية كأنك تمنح حاسوبك نظارات ذكية. بدلاً من رؤية "رقم" فقط، يرى الكمبيوتر "رقماً يجب أن يكون بين 0 و100". ثم تعمل أداة VerCors كـ حارس صارم، يتحقق في كل مرة يحاول فيها رقم ما دخول غرفة (أو متغير) ليتأكد من أنه يحمل بطاقة الهوية الصحيحة. إذا لم يكن كذلك، يوقف الحارس البرنامج قبل أن يتسبب في كارثة.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.