طريقة شكلية

التصنيف

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

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

إضافةً إلى ذلك، وكما هو الحال في سيمانتيك لغة البرمجة، فإن أنماط الطرق الشكلية يمكن أن يتم تصنيفها بشكل تقريبي كما يلي:

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

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

يمكن استخدام الطرق الشكلية على مجموعة من المستويات:

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

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

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

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

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

وفي هذا الصدد، يرى بعض الممارسين أن مجتمع الطرق الشكلية قد ركز بشكل زائد عن الحد على الشكلية الكاملة للمواصفة أو التصميم. وهم يؤكدون أن درجة التعبير عن اللغات المضمنة، إلى جانب درجة تعقيد الأنظمة التي يتم وضع نماذج لها، تجعل الشكلية الكاملة مهمة صعبة ومكلفة. وكبديل لذلك، تم اقتراح الكثير من الطرق الشكلية الخفيفة، والتي تركز على المواصفة الجزئية والتطبيق الذي يتم التركيز عليه. وتشتمل أمثلة هذه المنهجية الخفيفة للطرق الشكلية على ملاحظات نمذجة كائن لغة ألوي، وتوليف ديني لبعض أوجه تدوين زد مع التطوير المشتق من حالة الاستخدام، وأدوات CSK طريقة تطوير فيينا (VDM).

Foldoc:formal methods

وعلى صعيد آخر، Evidence on Formal Methods uses and impact on Industry Supported by the DEPLOY project (EU FP7)

كتابات أخرى

علاوةً على ذلك، Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, تايلور وفرانسيس, 2010, pages 308–320.

علاوةً على ذلك، جوناثان بوين 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 – 106-25, Chapman & Hall / سي آر سي بريس، رابطة مكائن الحوسبة, 2004.

علاوةً على ذلك، Jean François Monin and Michael G. Hinchey, Understanding formal methods, سبرنجر, 2003, ISBN 1-85233-247-6.