NASALib هو جهد تعاوني مستمر امتد لأكثر من 3 عقود، للمساعدة في الأبحاث المتعلقة بإثبات النظرية التي ترعاها وكالة ناسا (https://shemesh.larc.nasa.gov/fm/pvs/). وهو يتألف من مجموعة من عمليات التطوير الرسمية (أي المكتبات ) المكتوبة في نظام التحقق من النموذج الأولي (PVS)، والتي ساهم بها SRI وNASA وNIA ومجتمع PVS، ويحتفظ بها فريق الأساليب الرسمية في LaRC.
الإصدار الحالي من NASALib هو 7.1.2 (2023/09/01) ويتطلب PVS 7.1.
حاليًا، يتكون NASALib من 62 مكتبة عالية المستوى ، تحتوي على حوالي 38 ألف صيغة مثبتة إجمالاً.
| مكتبة | وصف |
|---|---|
| اتفاق | إطار لتحليل خوارزميات الكشف عن صراعات الحركة الجوية وحلها |
| affine_arith | إضفاء الطابع الرسمي على الحساب المتقارب واستراتيجية تقييم الدوال متعددة الحدود مع المتغيرات في المجالات الفاصلة |
| الجبر | المجموعات والأحادية والخواتم وما إلى ذلك |
| تحليل | التحليل الحقيقي، النهايات، الاستمرارية، المشتقات، التكاملات |
| آسيا والمحيط الهادئ | الدلالات الدلالية لبرمجة مجموعة الإجابات |
| الطيران | دعم التعريفات والخصائص الخاصة بالصيغ الرسمية المتعلقة بالطيران |
| برنشتاين | إضفاء الطابع الرسمي على كثيرات حدود برنشتاين متعددة المتغيرات |
| CCG | إضفاء الطابع الرسمي على معايير إنهاء الخدمة المتنوعة |
| معقد | أرقام معقدة |
| complex_alt | إضفاء الطابع الرسمي البديل على الأعداد المركبة |
| complex_integration | التكامل المعقد |
| co_structures | تسلسلات ذات أطوال معدودة محددة على أنها أنواع بيانات جبرية مشتركة |
| رسوم بيانية | الرسوم البيانية الموجهة: الدوائر، والأشجار الفرعية القصوى، والمسارات، وDAGs |
| ديسيلتر | المنطق الديناميكي التفاضلي |
| بالضبط_حقيقي_اريث | الحساب الحقيقي الدقيق بما في ذلك الدوال المثلثية |
| أمثلة | أمثلة على تطبيق الوظائف التي يوفرها NASALib |
| Extend_nnreal | ريالات غير سلبية ممتدة |
| fast_approx | تقريبيات الوظائف العددية القياسية |
| خطأ_التسامح | بروتوكولات التسامح مع الخطأ |
| يطفو | النقطة العائمة الحسابية |
| الرسوم البيانية | نظرية الرسم البياني |
| الفاصل الزمني_اريث | الفاصل الحسابي والتقريب العددي. يتضمن استراتيجيات رقمية تلقائية لحساب التقريبات العددية والفاصل الزمني للتحقق من مدى رضا وصحة الصيغ ذات القيمة الحقيقية الكمية. يتضمن هذا التطور إضفاء الطابع الرسمي على المنطق الزمني لفاصل ألين |
| ints | قسمة الأعداد الصحيحة، GCD، mod، التحليل الأولي، الحد الأدنى، الحد الأقصى |
| com.lebesgue | تكامل ليبيسج مع الاتصال بتكامل ريمان |
| جبر_خطي | الجبر الخطي |
| line_segments | قطع خطية ثنائية الأبعاد |
| com.lnexp | اللوغاريتمات والدوال الأسية والزائدة. والتعاريف الأساسية للوغاريتم والدوال الأسية والزائدة |
| LTL | المنطق الزمني الخطي |
| المصفوفات | المواصفات القابلة للتنفيذ لمصفوفات MxN. تتضمن هذه المكتبة حساب عمليات المصفوفة العكسية والأساسية مثل الجمع والضرب |
| Measure_Integration | جبر سيجما، التدابير، فوبيني-تونيلي ليماس |
| ميتيتارسكي | تكامل MetiTarski، وهو مُبرهن نظري آلي للوظائف ذات القيمة الحقيقية |
| metric_space | المجالات ذات مقياس المسافة والاستمرارية والاستمرارية الموحدة |
| mv_ana Analysis | التحليل الحقيقي متعدد المتغيرات: المعايير، والحدود، والاستمرارية، والمشتقات، والتحسين، وما إلى ذلك. |
| multi_poly | متعددات الحدود متعددة المتغيرات والمجموعات شبه الجبرية. |
| الاسمي | الاستدلال المعادلة الاسمية |
| أرقام | نظرية الأعداد الأولية |
| قصائد غنائية غنائية | المعادلات التفاضلية العادية |
| طلبات | أوامر مجردة، المشابك، نقاط الإصلاح |
| المضلعات | مضلعات ثنائية الأبعاد |
| polygon_merge | دمج المضلعات ثنائية الأبعاد دون توليد ثقوب |
| قوة | وظيفة الطاقة المعممة (بدون ln/exp) |
| احتمال | نظرية الاحتمالية |
| PVS0 | إضفاء الطابع الرسمي على المفاهيم الحسابية الأساسية |
| pvsio_utils | إضافات إلى PVSio، مكتبة PVS القياسية للرسوم المتحركة بمواصفات PVS |
| ريال | الجمع، sub، inf، sqrt على القيم الحقيقية، القيمة المطلقة، إلخ |
| ريمان | تكامل ريمان |
| سكوت | طوبولوجيا سكوت |
| مسلسل | متسلسلات القوى، اختبار المقارنة، اختبار النسبة، نظرية تايلور |
| set_aux | مجموعات الطاقة، والأوامر، والأصلية على مجموعات لا حصر لها. يتضمن الحقائق الوظيفية والعلائقية المبنية على بديهية الاختيار وعلاقات الصقل المبنية على علاقات التكافؤ |
| الأشكال | الأشكال ثنائية الأبعاد: مثلث، متوازي أضلاع، مستطيل، قطعة دائرية |
| sigma_set | الجمع على مجموعات لا نهائية معدودة |
| فرز | خوارزميات الفرز |
| الهياكل | المصفوفات المحدودة، والتسلسلات المحدودة، والحقائب، والعديد من الهياكل الأخرى |
| شتورم | إضفاء الطابع الرسمي على نظرية ستورم لكثيرات الحدود أحادية المتغير. يتضمن استراتيجيات sturm و mono-poly لإثبات العلاقات متعددة الحدود أحادية المتغير تلقائيًا خلال فترة زمنية حقيقية |
| تارسكي | إضفاء الطابع الرسمي على نظرية تارسكي لكثيرات الحدود أحادية المتغير. يتضمن استراتيجية tarski لإثبات أنظمة العلاقات متعددة الحدود أحادية المتغير تلقائيًا على الخط الحقيقي |
| طوبولوجيا | الاستمرارية، التماثل، المساحات المتصلة والمدمجة، مجموعات/وظائف بوريل |
| علم حساب المثلثات | علم المثلثات: التعاريف والهويات والتقريبات |
| TRS | أنظمة إعادة كتابة المصطلح وخوارزمية توحيد روبنسون |
| TU_games | ألعاب TU التعاونية |
| تحليل_vect | حدود واستمرارية ومشتقات الدوال المتجهة |
| ناقلات | ناقلات ثنائية الأبعاد وثلاثية الأبعاد ورباعية الأبعاد ونواقل الأبعاد |
| بينما | دلالات لغة البرمجة بينما |
يوفر NASALib أيضًا مجموعة من البرامج النصية التي تعمل على أتمتة العديد من المهام.
proveit (*) - يقوم بتشغيل PVS في الوضع الدفعيprovethem (*) - يعمل على proveit عدة مكتباتpvsio (*) - أداة مساعدة لسطر الأوامر لتشغيل المقيم الأرضي PVSio.prove-all - يقوم بتشغيل proveit في كل مكتبة في NASALib عن طريق تغليف provethem لتوفير نوع معين من التشغيل.cleanbin-all - تنظيف .pvscontext والملفات الثنائية من مكتبات PVS.find-all - يبحث عن سلاسل مطابقة لتعبيرات عادية معينة في مكتبات PVS.dependencygraph - يُنشئ رسمًا بيانيًا لتبعية المكتبة للمكتبات الموجودة في الدليل الحالي.dependency-all - إنشاء الرسوم البيانية التبعية لمكتبات PVS في المجلد الحالي.انقر هنا لمزيد من التفاصيل حول هذه البرامج النصية.
(*) تم تضمينه بالفعل في توزيع PVS 7.1.
NASALib (الإصدار 7.0.1) متوافق تمامًا مع VSCode-PVS، وهي واجهة رسومية حديثة لـ PVS تعتمد على Visual Studio Code. يمكن تثبيت أحدث إصدار من NASALib من VSCode-PVS.
بالنسبة لمستخدمي PVS المتقدمين، يتوفر إصدار التطوير من GitHub. لاستنساخ نسخة التطوير، اكتب الأمر التالي داخل الدليل حيث تم تثبيت PVS 7.0. من الآن فصاعدا، سيتم الإشارة إلى هذا الدليل باسم
$ git clone http://github.com/nasa/pvslib nasalib الأمر أعلاه سيضع نسخة من المكتبة في الدليل
تم الآن إهمال groups المكتبة . تم دمج مكتبة group في algebra . لا يزال يتم توفير رابط رمزي للتوافق مع الإصدارات السابقة، ولكن لا يُنصح باستخدامه. يجب استبدال كل إشارة إلى groups algebra .
تم الآن إهمال المكتبة trig_fnd . لا يزال يتم توفيره للتوافق مع الإصدارات السابقة، ولكن يجب استبداله بـ trig . مكتبة trig الجديدة، التي كانت بديهية، أصبحت الآن أساسية. ومع ذلك، على عكس trig_fnd ، تعتمد التعريفات المثلثية على سلسلة لا نهائية، بدلاً من التكاملات. يقلل هذا التغيير بشكل كبير من التحقق من نوع النظريات التي تتضمن الدوال المثلثية. لا ينبغي أن يكون للتغيير من trig_fnd إلى trig تأثير كبير في تطوراتك الرسمية نظرًا لأن أسماء التعريفات والمفردات هي نفسها. ومع ذلك، قد يكون استيراد النظرية مختلفًا بعض الشيء.
تطويرات PVS TCASII و WellClear و DAIDALUS متاحة الآن كجزء من توزيع GitHub WellClear. تطوير PVS PRECiSA متاح الآن كجزء من توزيع GitHub PRECiSA. تطوير PVS PolyCARP متاح الآن كجزء من توزيع GitHub PolyCARP.
تفترض التعليمات التالية أن NASALib موجود في الدليل
PVS_LIBRARY_PATH إذا لم يكن موجودًا، فقم بإنشاء هذا المتغير ومع مسار هذا الدليل كمحتوى فقط. عادةً ما يكون من المفيد جدًا أن تقوم أنظمة الصدفة الخاصة بك بإنشاء هذا المتغير عند بدء التشغيل. ولتحقيق هذه الغاية، واعتمادًا على الصدفة الخاصة بك، قد ترغب في إضافة أحد الأسطر التالية في البرنامج النصي لبدء التشغيل. بالنسبة لـ C Shell (csh أو tcsh)، يمكنك إضافة هذا السطر في ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " بالنسبة لـ Borne Shell (bash أو sh)، أضف هذا السطر إما في ~/.bashrc أو ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " إذا كان لديك تثبيت سابق لبرنامج NASALib، فقم إما بإزالة الملف ~/.pvs.lisp أو إذا كان لديك تكوين خاص في هذا الملف، فقم بإزالة السطر التالي
( load " /nasalib/pvs-patches.lisp " ) أخيرًا، انتقل إلى الدليل
سيقوم أمر install-scripts بتحديث البرامج النصية NASALib وتثبيتها حسب الحاجة.
$ ./install-scriptsالإصدارات الأقدم من NASALib متاحة على http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
لقد تطور موقع NASALib على مر السنين بفضل مساهمة العديد من الأشخاص، من بينهم:
إذا قمنا بإسناد تطوير PVS بشكل غير صحيح أو كنت قد ساهمت في NASALib ولم يتم تضمين اسمك هنا، فيرجى إخبارنا بذلك.
إذا كنت تريد المساهمة يرجى قراءة هذا الدليل.
NASALib عبارة عن مجموعة من المواصفات الرسمية التي ظل معظمها في الملكية العامة لعدة سنوات. لا يزال فريق الأساليب الرسمية في NASA LaRC يحافظ على هذه التطورات. بالنسبة للتطورات التي أجراها في الأصل فريق الأساليب الرسمية، تعتبر هذه التطورات بحثًا أساسيًا لا يشكل برنامجًا. قد تحتوي المساهمات المقدمة من الآخرين على تراخيص معينة، وهي مدرجة في الملف top.pvs في كل دليل على حدة. في حالة الشك، يرجى الاتصال بمطوري كل مساهمة، والمدرجين أيضًا في هذا الملف.
تعد تصحيحات PVS، المضمنة في الدليل pvs-patches ، جزءًا من كود مصدر PVS وهي مغطاة بترخيص PVS مفتوح المصدر.
تتطلب بعض استراتيجيات الإثبات أدوات بحث من طرف ثالث، على سبيل المثال، MetiTarski وZ3. وللتيسير، تم تضمينها في هذا المستودع بإذن من مؤلفيها. يتم أيضًا تضمين تراخيص هذه الأدوات حسب الاقتضاء.
استمتع بها.
فريق الأساليب الرسمية في LaRC
سيزار مونيوز ماريانو موسكاتو
