نظام مود

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

برنامج Maude هو برنامج مجاني، وتتوفر دروس تعليمية عنه عبر الإنترنت. تم تطويره في الأصل في معهد SRI الدولي ، ^{[ 1 ]} ولكنه يُطوَّر الآن من خلال تعاون متنوع بين الباحثين. ^{[ 2 ]}

يهدف برنامج Maude إلى حل مجموعة مختلفة من المشكلات التي تواجهها لغات البرمجة الإجرائية التقليدية مثل C و Java و Perl . فهو أداة استدلال رسمي، تساعدنا على التحقق من أن الأمور تسير على النحو الأمثل، وتُبين لنا أسباب عدم صحتها في حال تحقق ذلك. بعبارة أخرى، يُمكّننا Maude من تعريف مفهوم ما تعريفًا رسميًا بطريقة مجردة للغاية (دون الخوض في تفاصيل كيفية تمثيل البنية داخليًا وما إلى ذلك)، ولكن يُمكننا وصف ما يُعتقد أنه مكافئ لنظريتنا ( المعادلات ) والتغيرات التي قد تطرأ عليها ( قواعد إعادة الكتابة ).

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

يُفترض أن تكون معادلات الاختزال متصلة ومنتهية . أما قواعد إعادة الكتابة فلا تخضع لهذا القيد.

عندما تُنفّذ Maude، فإنها تُعيد كتابة الحدود وفقًا للمعادلات وقواعد إعادة الكتابة. تُعيد Maude كتابة الحدود وفقًا للمعادلات كلما وُجد تطابق بين الحدود المغلقة التي يُراد إعادة كتابتها (أو اختزالها) والطرف الأيسر من معادلة في مجموعة المعادلات. التطابق في هذا السياق هو استبدال المتغيرات في الطرف الأيسر من المعادلة بحيث تُصبح مُطابقة للحد الذي يُراد إعادة كتابته/اختزاله. يمكن أن تكون المعادلات وقواعد إعادة الكتابة قواعد شرطية ، مما يعني أنه يجب أن تُحقق معايير مُعينة ليتم تطبيقها على الحد (إلى جانب مُجرد مُطابقة الطرف الأيسر من قاعدة إعادة الكتابة).

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

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

استخدمت شركة RTX (المعروفة سابقًا باسم Raytheon Technologies) برنامج Maude لكتابة "إحدى أولى الأدوات العامة والنمطية لتجربة تصميم أنظمة الاتصالات المخفية (HCS) على نطاقات عملية". ^{[ 3 ]}

• Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer and Quesada, 1998. Maude as a Metalanguage , in Proc. 2nd International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 15, Elsevier.
• مارتي-أوليت وخوسيه ميسيغوير ، 2002. إعادة كتابة المنطق: خارطة الطريق وقائمة المراجع . علوم الحاسوب النظرية 285(2):121-154.
• مارتي-أوليت وخوسيه ميسيغوير ، 1993-2000. إعادة كتابة المنطق كإطار منطقي ودلالي . ملاحظات إلكترونية في علوم الحاسوب النظرية 4، إلسيفير.
• كلافيل، دوران، إيكر، لينكولن، مارتي-أوليت، ميسيغوير، وتالكوت (2007). كل شيء عن مود - إطار منطقي عالي الأداء: كيفية تحديد وبرمجة والتحقق من الأنظمة في منطق إعادة الكتابة (ملف PDF) . سبرينغر. ISBN 978-3-540-71940-3.{{cite book}}: صيانة CS1: أسماء متعددة: قائمة المؤلفين ( رابط )

• الصفحة الرئيسية لمود في جامعة إلينوي في أوربانا-شامبين؛
• الصفحة الرئيسية لأداة Real-Time Maude مؤرشفة بتاريخ 2011-05-14 في Wayback Machine ، تم تطويرها بواسطة Peter Csaba Ölveczky؛
• مقدمة عن مود بقلم نيل هارمان، جامعة سوانسي ( أخطاء مطبعية )
• بنية موزعة قائمة على السياسات والأهداف مكتوبة بلغة Maude من قبل SRI International.
• Maude for Windows ، وهو برنامج تثبيت Maude لنظام التشغيل Windows، و Maude Development Tools ، وهو المكون الإضافي لـ Maude Eclipse الذي طوره مشروع MOMENT في جامعة فالنسيا التقنية (إسبانيا).