لغة المواصفات
لغة المواصفات هي لغة شكلية في علم الحاسوب تستخدم أثناء تحليل الأنظمة وتحليل المتطلبات وتصميم الأنظمة لوصف نظام على مستوى أعلى بكثير من لغة البرمجة، والتي تستخدم لإنتاج التعليمات البرمجية القابلة للتنفيذ لنظام ما.
نظرة عامة
عدللا يتم تنفيذ لغات المواصفات بشكل مباشر بشكل عام. والمقصود منها أن تصف ما، وليس كيف. في الواقع، يعتبر خطأ إذا كانت مواصفات المتطلبات تشوش مع تفاصيل التنفيذ غير الضرورية.
ومن الافتراضات الأساسية الشائعة للعديد من الأساليب المواصفات أن البرامج هي على غرار الهياكل الجبرية أو النظرية النموذجية التي تشمل مجموعة من مجموعات من قيم البيانات جنبًا إلى جنب مع وظائف على تلك المجموعات. يتزامن هذا المستوى من التجريد مع الرأي القائل بأن صحة سلوك الإدخال/الإخراج للبرنامج لها الأسبقية على كافة خصائصه الأخرى.
في نهج الملكية المنحى للمواصفات (التي اتخذت على سبيل المثال من قبل CASL)، ومواصفات البرامج تتكون أساسًا من البديهيات المنطقية، وعادة ما يكون في نظام منطقي فيه المساواة دورا بارزًا، واصفًا الخصائص التي يتعين على وظائف لتلبيتها، في كثير من الأحيان فقط من خلال العلاقة المتبادلة بينهما. وهذا على النقيض مما يسمى بالمواصفات الموجهة نحو النموذج في أطر مثل VDM وZ، والتي تتكون من تحقيق بسيط للسلوك المطلوب.
ويجب أن تخضع المواصفات لعملية صقل (ملء تفاصيل التنفيذ) قبل أن يتسنى تنفيذها فعلياً. نتيجة عملية التحسين هذه هي خوارزمية قابلة للتنفيذ، والتي يتم إما صياغتها بلغة برمجة، أو في مجموعة فرعية قابلة للتنفيذ من لغة المواصفات في متناول اليد. على سبيل المثال، خطوط أنابيب هارتمان، عند تطبيقها بشكل صحيح، يمكن اعتبارها مواصفات تدفق البيانات التي هي قابلة للتنفيذ مباشرة. مثال آخر هو نموذج الممثل الذي لا يحتوي على محتوى تطبيق محدد ويجب أن يكون متخصصاً ليكون قابل للتنفيذ.
استخدام مهم للغات المواصفات هو تمكين إنشاء براهين رياضية من صحة البرنامج (انظر نظرية بروفير).
لغات
عدلانظر أيضًا
عدلمراجع
عدل- ^ Fuchs، Norbert E.؛ Schwertel، Uta؛ Schwitter، Rolf (1998). "Attempto Controlled English—not just another logic specification language" (PDF). International Workshop on Logic Programming Synthesis and Transformation. Lecture Notes in Computer Science. Springer. ج. 1559. ص. 1–20. DOI:10.1007/3-540-48958-4_1. ISBN:978-3-540-65765-1.[وصلة مكسورة]
- ^ Linden، Theodore؛ Lawrence Markosian (1989). "Transformational Synthesis Using Refine". في Richer، Mark (المحرر). AI Tools and Techniques. Ablex. ص. 261–286. ISBN:0-89391-494-0. اطلع عليه بتاريخ 2014-07-06.
