كتب formal methods
اذا لم تجد ما تبحث عنه يمكنك استخدام كلمات أكثر دقة.
الأساليب الشكلية (معلومة)
الأساليب الشكلية هي المصطلح المطبق على تحليل البرمجيات (والعتاد الحاسوبي) الذي تُستخدم أساليب رياضية دقيقة حصرًا للحصول على نتائجه. تشمل التقنيات الرياضية المستخدمة دلالات ترميزية، ودلالات بديهية، ودلالات تشغيلية والتفسير المجرد.
يمكن من خلال الحد المباشر لمسألة التوقف، إثبات أن عثور (أي لغة كاملة حسب تورينغ) على جميع أخطاء زمن التنفيذ المحتملة في برنامج كيفي (أو أي نوع من خرق المواصفات في النتيجة النهائية للبرنامج عمومًا) غير قابل للحسم: لا توجد طريقة آلية يمكنها دائمًا الإجابة بصدق عمّا إذا كان البرنامج الكيفي سيظهر أو لن يظهر أخطاء زمن التنفيذ. تعود هذه النتائج إلى أعمال تشرتش وغودل وتورنغ في ثلاثينيات القرن العشرين (انظر: مسألة التوقف ونظرية رايس). مثل العديد من الأسئلة غير القابلة للحسم، يمكن محاولة تقديم حلول تقريبية مفيدة.
تتضمن بعض تقنيات تنفيذ التحليل الساكن الشكلي ما يلي:
- التفسير المجرد، لنمذجة تأثير كل تعليمة على حالة الآلة المجردة (أي «يُنفذ» البرمجيات بناءً على الخصائص الرياضية لكل تعليمة وتصريح). تقارب هذه الآلة المجردة سلوكيات النظام بشكل مفرط: وبالتالي يصبح نظام المجرد أسهل في التحليل، على حساب عدم الاكتمال (ليس كل خاصية حقيقية في النظام الأصلي حقيقة في النظام المجرد). ولكن إذا أُجري التفسير المجرد على النحو الصحيح يكون سليمًا (يمكن تعيين كل خاصية حقيقية للنظام التجريدي إلى خاصية حقيقية للنظام الأصلي). يعتمد ملحق تحليل قيمة إطار التحليل المعياري لبرامج سي (فريما سي). وأداة التحليل بوليسبيس بشدة على التفسير المجرد.
- تحليل تدفق البيانات، تقنية تعتمد على الشبكية لجمع المعلومات عن مجموعة القيم المحتملة؛
- منطق هور، نظام شكلي مع مجموعة من القواعد المنطقية للتفكير بدقة حول صحة برامج الحاسوب. يوجد أداة دعم لبعض الغات البرمجة (مثل لغة البرمجة سبارك (مجموعة فرعية من لغة البرمجة أيدا) ولغة جافا للنمذجة -جاي إم إل- باستخدام المدقق الساكن الموسع للجافا (إي إس سي/ جافا) والمدقق الساكن الموسع لجافا 2 ومحلق إطارالتحليل المعياري لبرامج سي ذات الشرط المسبق الأضعف (دبليو بّي) للغة سي الموسعة بلغة المحاكاة المستمرة المتقدمة إيه سي إس إل (لغة مواصفات سي حسب المعهد الوطني الأمريكي للمعايير/آيزو).
- التحقق من النموذج، يراعي الأنظمة ذات الحالات المنتهية أو يمكن اختزالها إلى حالة منتهية عن طريق التجريد؛
- التنفيذ الرمزي، مستخدم أيضًا لاشتقاق العبارات الرياضية التي تمثل قيمة المتغيرات المتحولة عند نقاط معينة في الكود.
