طريقة شكلية

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

وأفضل وصف للطرق الشكلية هو أنها تطبيق يتميز بالتنوع واسع النطاق بشكل كبير لأساسيات المعلوماتية النظرية، على وجه الخصوص حسابات المنطق واللغات الشكلية ونظرية التشغيل الذاتي وسيمانتك البرامج، ولكن كذلك نظام الأنواع وأنواع البيانات الجبرية للمشكلات فيما يتعلق بمواصفات الأجهزة والتحقق منها.Monin, pp.3-4
 التصنيف 
يمكن استخدام الطرق الشكلية على مجموعة من المستويات:

المستوى 0: المواصفات الشكلية يمكن تنفيذها وبالتالي يمكن تطوير برنامج منها بشكل غير شكلي. وقد أطلق على ذلك اسم الطرق الشكلية الخفيفة. ويمكن أن يكون هذا الخيار هو أفضل الخيارات من ناحية التكلفة في العديد من الحالات.

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

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

وهناك المزيد من المعلومات حول هذا الأمر أدناه.

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

 الطرق الشكلية الخفيفة 

يرى بعض الممارسين أن مجتمع الطرق الشكلية قد ركز بشكل زائد عن الحد على الشكلية الكاملة للمواصفة أو التصميم.دانييل جاكسون and جانيت وينغ, "Lightweight Formal Methods", IEEE Computer, April 1996 Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003  وهم يؤكدون أن درجة التعبير عن اللغات المضمنة، بالإضافة إلى درجة تعقيد الأنظمة التي يتم وضع نماذج لها، تجعل الشكلية الكاملة مهمة صعبة ومكلفة. وكبديل لذلك، تم اقتراح العديد من الطرق الشكلية الخفيفة، والتي تركز على المواصفة الجزئية والتطبيق الذي يتم التركيز عليه. وتشتمل أمثلة هذه المنهجية الخفيفة للطرق الشكلية على ملاحظات نمذجة كائن لغة ألوي،Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290  وتوليف ديني لبعض أوجه تدوين زد مع التطوير المشتق من حالة الاستخدام،Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6. وأدوات CSK طريقة تطوير فيينا (VDM).Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998 

 انظر أيضًا 
 الأشخاص المعتمدون على الطرق الشكلية
 هندسة البرمجيات

 المراجع 

 كتابات أخرى 

 Jean François Monin and Michael G. Hinchey, Understanding formal methods, سبرنجر, 2003, ISBN 1-85233-247-6.
 جوناثان بوين and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering,Chapter 106, pages 106-1&nbsp;– 106-25, Chapman & Hall / سي آر سي بريس، رابطة مكائن الحوسبة, 2004.
 Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, تايلور وفرانسيس, 2010, pages 308–320.

 وصلات خارجية 
 Formal Methods Europe (FME)
 Formal method keyword on Microsoft Academic Search
 Foldoc:formal methods
 Evidence on Formal Methods uses and impact on Industry Supported by the DEPLOY project (EU FP7)

تصنيف:طرق شكلية
تصنيف:لغات المواصفات
تصنيف:علم الحاسوب النظري