ماتيتا

📅 آخر تحديث: ٣٠ يوليو ٢٠٢٦
✍️ نُشر في: ٣٠ يوليو ٢٠٢٦
الموسوعة الحرة

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

يعتمد ماتيتا على نظام نوع تابع يُعرف باسم حساب الإنشاءات (الاستقرائية) (وهو مشتق من حساب الإنشاءات )، وهو متوافق إلى حد ما مع روك .

كلمة "ماتيتا" تعني "قلم رصاص" بالإيطالية (وهي أداة تحرير بسيطة وشائعة الاستخدام). وهو تطبيق صغير وبسيط نسبيًا، [ 2 ] مصمم بحيث يسهل على الطلاب فهم بنيته وبرمجياته، مما يجعله أداة مناسبة بشكل خاص لاختبار الأفكار والحلول المبتكرة. تعتمد ماتيتا على نمط تحرير قائم على التكتيكات ؛ حيث يتم إنشاء كائنات إثبات ( مشفرة بصيغة XML ) للتخزين والتبادل.

الميزات الرئيسية

المتغيرات الوجودية موجودة أصلاً في ماتيتا، مما يسمح بإدارة أبسط للأهداف التابعة. [ 3 ]

يقوم ماتيتا بتنفيذ خوارزمية استدلال نوع ثنائية الاتجاه [ 4 ] تستغل كل من الأنواع المستنتجة والمتوقعة.

يتم تعزيز قوة نظام استنتاج النوع (المحسن) بشكل أكبر من خلال آلية التلميحات [ 5 ] التي تساعد في توليف الموحدات في حالات معينة يحددها المستخدم.

يدعم ماتيتا استراتيجية متطورة لإزالة الغموض [ 6 ] تعتمد على حوار بين المحلل اللغوي ومدقق الأنواع .

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

التطبيقات

تم توظيف ماتيتا في مشروع CerCo (التعقيد المعتمد): وهو مشروع أوروبي ضمن برنامج FP7 يركز على تطوير مترجم تم التحقق منه رسميًا ويحافظ على التعقيد من مجموعة فرعية كبيرة من لغة C إلى لغة التجميع الخاصة بمعالج MCS-51 .

الوثائق

يقدم البرنامج التعليمي ماتيتا [ 8 ] مقدمة عملية للوظائف الرئيسية لبرنامج ماتيتا التفاعلي لإثبات النظريات، ويقدم جولة إرشادية من خلال مجموعة من الأمثلة غير التافهة في مجال مواصفات البرامج والتحقق منها .

انظر أيضاً

مراجع

  1. ↑ أندريا أسبيرتي، ويلمر ريتشوتي، كلاوديو ساسيردوتي كوين، إنريكو تاسي. "مبرهنة ماتيتا التفاعلية": CADE-23، LNCS 6803، 2011، الصفحات من 64 إلى 69 .
  2. ^ أسبرتي، أ. ريتشوتي، دبليو؛ ساسيردوتي كوين، سي. تاسي، إي. (2009). "نواة مدمجة لحساب التفاضل والتكامل للإنشاءات الاستقرائية" . سادهانا . 34 : 71 – 144. دوى : 10.1007 / s12046-009-0003-3 .
  3. ↑ أندريا أسبيرتي، ويلمر ريتشوتي، سي ساسيردوتي كوين، إنريكو تاسي. "نوع جديد من التكتيكات": التقرير الفني UBLCS-2009-14. يونيو 2009.
  4. ↑ أندريا أسبرتي، ويلمر ريتشوتي، سي ساسيردوتي كوين، إنريكو تاسي. "خوارزمية تحسين ثنائية الاتجاه لحساب الإنشاءات (الاستقرائية) المشتركة". الأساليب المنطقية في علوم الحاسوب، المجلد 8، العدد 1
  5. ↑ أندريا أسبيرتي، ويلمر ريتشوتي، سي ساسيردوتي كوين، إنريكو تاسي. "تلميحات في التوحيد": LNCS V.5674, 2009، الصفحات 84-98
  6. ^ كلاوديو ساسيردوتي كوين، ستيفانو زاشيرولي “التحليل الغامض الفعال للصيغ الرياضية” LNCS V.3119، 2004، ص 347-362
  7. ^ كلاوديو ساسيردوتي كوين، إنريكو تاسي، ستيفانو زاشيرولي “Tinycals: خطوة بخطوة تكتيكات” ENTCS V.174، n.2، 2007، الصفحات 125-142
  8. ^ أندريا أسبيرتي، ويلمر ريتشوتي، كلاوديو ساسيردوتي كوين “برنامج ماتيتا التعليمي” مجلة الاستدلال الرسمي، V.7، ن. 2، 2014، الصفحات 91-199
  • مساعد ماتيتا للتدقيق في آلة Wayback (تمت أرشفته في 2023-02-04)
  • مشروع CerCo على موقع Wayback Machine (تمت أرشفته في 21-05-2022)