نظام التحقق من النموذج الأولي
نظام التحقق من النموذج الأولي ( PVS ) هو لغة مواصفات متكاملة مع أدوات الدعم وبرنامج إثبات النظريات الآلي ، تم تطويره في مختبر علوم الحاسوب التابع لمعهد SRI الدولي في مينلو بارك، كاليفورنيا .
تعتمد PVS على نواة تتألف من امتداد لنظرية الأنواع لتشرش مع الأنواع التابعة ، وهي في جوهرها منطق كلاسيكي عالي الرتبة مُنمذج. تشمل الأنواع الأساسية أنواعًا غير مُفسَّرة يُمكن للمستخدم تعريفها، وأنواعًا مُدمجة مثل القيم المنطقية، والأعداد الصحيحة، والأعداد الحقيقية، والأعداد الترتيبية. تشمل مُنشئات الأنواع الدوال، والمجموعات، والصفوف، والسجلات، والتعدادات، وأنواع البيانات المجردة. يُمكن استخدام الأنواع الفرعية للمسندات والأنواع التابعة لفرض قيود؛ وقد تُفرض على هذه الأنواع المُقيدة التزامات إثبات (تُسمى شروط صحة النوع أو TCCs) أثناء فحص النوع. تُنظَّم مواصفات PVS في نظريات مُعَلمة.
تم تنفيذ النظام بلغة Common Lisp ، وتم إصداره بموجب رخصة جنو العمومية العامة (GPL).
انظر أيضاً
مراجع
روابط خارجية
- موقع PVS الإلكتروني في مختبر علوم الحاسوب التابع لمعهد SRI الدولي
- ملخص لـ PVS من تأليف جون راشبي في قاعدة بيانات الاستدلال الآلي لمايكل كولهاس وكارولين تالكوت
- PVSgym هي بيئة تعلم معزز لـ PVS
- لغات المواصفات الرسمية
- مساعدو التدقيق اللغوي
- اللغات ذات الكتابة المعتمدة
- لغة البرمجة ليسب
- برامج لغة البرمجة Common Lisp
- برامج إثبات النظريات المجانية
- برنامج مجاني مكتوب بلغة ليسب
- برمجيات SRI الدولية
- برنامج يستخدم رخصة جنو العمومية العامة
- مواضيع لغات البرمجة
- نماذج منطقية