التحقق الرسمي ومساعدو البراهين
يُثبت التحقق الرسمي، من خلال برهان رياضي مدقق آليًا، أن البرنامج يفي بمواصفاته؛ ومساعدو البراهين هي الأدوات التي تبني وتدقق هذه البراهين.
Definition
التحقق الرسمي هو بناء برهان صارم ومدقق آليًا بأن النظام يفي بمواصفات رسمية، ومساعد البرهان هو برنامج يساعد المستخدم على تطوير مثل هذه البراهين ويتحقق ميكانيكيًا من صحتها.
Scope
يغطي هذا الموضوع التحقق الاستنتاجي وإثبات النظريات التفاعلي: مساعدو البراهين القائمة على نظرية الأنواع أو المنطق عالي الرتبة (مثل Coq و Isabelle و Lean و Agda)، ومنهج LCF للبرهان الموثوق، وأساس القضايا كأنواع، وأتمتة البراهين والتكتيكات، والمصنوعات الأثرية الموثقة البارزة بما في ذلك المترجمات ونواة أنظمة التشغيل.
Core questions
- كيف يمكن إثبات صحة وظيفية كاملة والتحقق منها آليًا؟
- لماذا تُعد مساعدات البراهين جديرة بالثقة، وما هو أساس الحوسبة الموثوق به؟
- كيف يربط تطابق كاري-هاورد بين البراهين والبرامج؟
- ما الذي يتطلبه الأمر للتحقق من أنظمة حقيقية مثل المترجمات والنوى؟
Key theories
- منهج LCF للبرهان الموثوق
- قدمت Edinburgh LCF لغوردون وميلنر ووادزورث نواة برهان موثوقة صغيرة يجب أن تمر جميع النظريات من خلالها، بحيث لا يمكن حتى للأتمتة المعقدة أن تنتج براهين غير سليمة.
- مترجم موثق (CompCert)
- CompCert لـ ليروي هو مترجم لغة C أُثبتت صحته في مساعد برهان، مع نظرية مدققة آليًا بأن الكود المُنشأ يحسن دلالات البرنامج المصدر.
- نواة نظام تشغيل موثقة (seL4)
- أنتج كلاين وزملاؤه برهانًا مدققًا آليًا للصحة الوظيفية للنواة المصغرة seL4، مما يدل على التحقق الشامل من برامج الأنظمة منخفضة المستوى.
Clinical relevance
يوفر التحقق الآلي أعلى مستوى من الضمان المتاح للبرامج الحيوية، وينتج مترجمات ونوى ومكتبات تشفير بضمانات مثبتة بدلاً من الثقة القائمة على الاختبار. كما تُستخدم مساعدات البراهين بشكل متزايد لإضفاء الطابع الرسمي على الرياضيات نفسها.
History
بدأ إثبات النظريات التفاعلي مع Edinburgh LCF في السبعينيات، والذي شكلت لغته الوصفية ML ونواته الموثوقة الأنظمة اللاحقة. نضجت المساعدات القائمة على نظرية الأنواع مثل Coq و Agda وأنظمة المنطق عالي الرتبة مثل Isabelle/HOL على مدى العقود التالية، وبلغت ذروتها في مصنوعات أثرية موثقة بارزة: مترجم CompCert (2009) ونواة seL4 (2009).
Debates
- تكلفة التحقق مقابل الضمان المكتسب
- يتطلب بناء براهين مدققة آليًا للأنظمة الكبيرة جهدًا هائلاً، مما يثير نقاشًا حول متى يكون التحقق الكامل مبررًا مقابل متى تكون الأساليب الأخف وزنًا كافية، ومقدار ما يمكن أتمتته من البرهان.
Key figures
- Robin Milner
- Michael Gordon
- Xavier Leroy
- Gerwin Klein
- Robert Harper
Related topics
Seminal works
- gordon1979
- leroy2009
- klein2009
- harper2016
Frequently asked questions
- ما هو مساعد البرهان؟
- مساعد البرهان هو برنامج يقوم فيه المستخدم ببناء براهين رسمية بشكل تفاعلي بينما يتحقق النظام ميكانيكيًا من كل خطوة، بحيث يكون البرهان المكتمل موثوقًا به وصولًا إلى نواة صغيرة ومُدققة جيدًا.
- كيف يختلف التحقق من البرنامج عن اختباره؟
- يتحقق الاختبار من السلوك على مدخلات مختارة ويمكنه فقط الكشف عن وجود الأخطاء، بينما يثبت التحقق الرسمي صحة البرنامج لجميع المدخلات المسموح بها في المواصفات، مما يؤكد عدم وجود الأخطاء المحددة.