فحص ثابت موسع

📅 آخر تحديث: ١٩ يوليو ٢٠٢٦
✍️ نُشر في: ١٩ يوليو ٢٠٢٦
الموسوعة الحرة

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

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

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

بدأ استخدام الفحص الثابت الموسع في لغة ESC/Modula-3 [ 4 ] ، ولاحقًا في لغة ESC/Java . وتعود جذوره إلى تقنيات فحص ثابت أبسط، مثل تصحيح الأخطاء الثابت [ 5 ] أو أدوات lint و FindBugs . وقد تبنت العديد من اللغات الأخرى تقنية ESC، بما في ذلك Spec# و SPARKada و VHDL VSPEC. ومع ذلك، لا توجد حاليًا لغة برمجة واسعة الانتشار توفر فحصًا ثابتًا موسعًا في بيئة التطوير الأساسية الخاصة بها.

انظر أيضاً

مراجع

  1. ↑ سي. فلانغان، كيه آر إم لينو، إم. ليليبريدج، جي. نيلسون، جيه بي ساكس ، وآر. ستاتا. "التحقق الثابت الموسع للغة جافا". في وقائع مؤتمر تصميم وتنفيذ لغات البرمجة ، الصفحات 234-245، 2002. doi: http://doi.acm.org/10.1145/512529.512558
  2. 1 2 "الفحص الثابت الموسع" . UWTV . تم الاسترجاع في 1 فبراير 2012 .{{cite web}}: CS1 maint: deprecated archiveal service ( link )
  3. ↑ بابيتش، دوماغوي؛ هو، آلان ج. (2008). كاليستو: فحص ثابت موسع قابل للتوسع ودقيق . وقائع المؤتمر الدولي لهندسة البرمجيات (ICSE). مطبعة ACM. doi : 10.1145/1368088.1368118 .
  4. ↑ روستان، ك.؛ لينو، م.؛ نيلسون، جريج (1998). "مدقق ثابت موسع لـ modula-3". سلسلة محاضرات في علوم الحاسوب - المؤتمر الدولي حول بناء المترجمات . سبرينغر. ص 302-305 . doi : 10.1007/bfb0026441 . ISBN  978-3-540-64304-3ISSN 0302-9743​​ 
  5. ↑ فلاناغان، كورماك؛ فلات، ماثيو؛ كريشنامورثي، شري رام؛ ويريش، ستيفاني؛ فيليسين، ماتياس (1996). "اكتشاف الأخطاء في شبكة ثوابت البرنامج" (ملف PDF) . إشعارات ACM SIGPLAN . 31 (5). رابطة آلات الحوسبة (ACM): 23-32 . doi : 10.1145/249069.231387 . ISSN 0362-1340 . 

للمزيد من القراءة

  • كورماك فلانغان؛ ك. روستان م. لينو، مارك ليليبريدج، غريغ نيلسون، جيمس ب. ساكس، رايمي ستاتا (2002). "التحقق الثابت الموسع للغة جافا". وقائع مؤتمر ACM SIGPLAN 2002 حول تصميم لغات البرمجة وتنفيذها . ص  234. doi : 10.1145/512529.512558 . ISBN 978-1581134636. S2CID 47141042 . {{cite book}}: صيانة CS1: أسماء متعددة: قائمة المؤلفين ( رابط )
  • بابيتش، دوماغوي؛ هو، آلان ج. (2008). "كاليستو". وقائع المؤتمر الدولي الثالث عشر لهندسة البرمجيات - ICSE '08 . ص  211. doi : 10.1145/1368088.1368118 . ISBN 9781605580791. S2CID 62868643 . 
  • تشيس، بي في (2002). "تحسين أمن الحاسوب باستخدام الفحص الثابت الموسع". وقائع ندوة IEEE للأمن والخصوصية لعام 2002. الصفحات 160-173 . CiteSeerX 10.1.1.15.2090 . doi : 10.1109/SECPRI.2002.1004369 . ISBN   978-0-7695-1543-4. S2CID 12067758 . 
  • ريو، فريدريك؛ شالين، باتريس (2006). "تحسين جودة تطبيقات المؤسسات القائمة على الويب باستخدام الفحص الثابت الموسع: دراسة حالة" . الملاحظات الإلكترونية في علوم الحاسوب النظرية . 157 (2): 119-132 . doi : 10.1016/j.entcs.2005.12.050 . ISSN 1571-0661 . 
  • جيمس، بيري ر.؛ تشالين، باتريس (2009). "فحص ثابت موسع أسرع وأكثر شمولاً للغة نمذجة جافا". مجلة الاستدلال الآلي . 44 ( 1-2 ): 145-174 . CiteSeerX 10.1.1.165.7920 . doi : 10.1007/s10817-009-9134-9 . ISSN 0168-7433 . S2CID 14996225 .   
  • شو، دانا ن. (2006). "التحقق الثابت الموسع للغة هاسكل". وقائع ورشة عمل ACM SIGPLAN لعام 2006 حول هاسكل . ص  48. CiteSeerX 10.1.1.377.3777 . doi : 10.1145/1159842.1159849 . ISBN  978-1595934895. S2CID 1340468 . 
  • لينو، ك.، وروستان، م. (2001). "الفحص الثابت الموسع: منظور عشر سنوات". المعلوماتية . سلسلة محاضرات في علوم الحاسوب. المجلد  2000. الصفحات 157-175 . doi : 10.1007/3-540-44577-3_11 . ISBN  978-3-540-41635-7.
  • ديتليفز، ديفيد ل.؛ لينو، ك.؛ روستان م.؛ نيلسون، جريج؛ ساكس، جيمس ب. (1998). "الفحص الثابت الموسع". تقرير بحثي لشركة كومباك إس آر سي (159).