لغة البرمجة PVS، والتي تعرف باسم “نظام التحقق من النماذج الأولية” بالإنجليزية (Prototype Verification System)، هي لغة مواصفات متكاملة مع أدوات الدعم وأداة إثبات أنظمة آلية متطورة، تم تطويرها في مختبر علوم الحاسوب في شركة SRI International في منطقة مينلو بارك بولاية كاليفورنيا، الولايات المتحدة الأمريكية. تعتمد PVS على نواة تتكون من توسيع لنظرية الأنواع للكنيسة مع الأنواع التابعة، وهي في جوهرها منطق تصنيفي عالي النظام. تشمل الأنواع الأساسية أنواعًا غير مفسرة يمكن للمستخدم إدخالها، وأنواع مضمنة مثل القيم البولية، والأعداد الصحيحة، والأعداد الحقيقية، والترتيبيات. يتضمن بناء الأنواع الدوال والمجموعات والأزواج والسجلات والتعدادات وأنواع البيانات النموذجية. يمكن استخدام أنواع الفرعية القضائية والأنواع التابعة لإدخال القيود؛ يمكن أن تتسبب هذه الأنواع المقيدة في التزامات إثبات (تسمى شروط صحة النوع أو TCCs) أثناء فحص الأنواع. تُنظم المواصفات في PVS إلى نظريات معلمة. تم تنفيذ النظام بلغة Common Lisp، وتم إصداره بموجب ترخيص GNU General Public License (GPL).
تتميز PVS بقدرتها على تحليل وإثبات صحة النماذج الأولية بشكل دقيق وموثوق به. يتمثل أحد السمات البارزة لهذه اللغة في قدرتها على تنظيم المواصفات في نظريات معلمة، مما يسهل فهم وإدارة المشاريع الضخمة. بالإضافة إلى ذلك، توفر PVS مجموعة واسعة من الأنواع والمعالجات الرياضية، بما في ذلك الدوال والأعداد الحقيقية والمجموعات، مما يجعلها ملائمة للتعامل مع مجموعة متنوعة من المشاكل في البرمجة والهندسة الرياضية.
يمكن الاطلاع على المزيد من المعلومات حول PVS عبر الرابط التالي إلى صفحتها على ويكيبيديا: نظام التحقق من النماذج الأولية على ويكيبيديا.