anthem 1

النشيد

ترجمة برامج مجموعة الإجابات إلى لغة إثبات النظرية من الدرجة الأولى

حالة هذا المشروع

ملحوظة

أنت تنظر حاليًا إلى الإصدار 1 من anthem ، الذي أنشأه باتريك لون ولم يعد قيد التطوير. لن يتم إجراء أي التزامات أخرى لهذا المستودع.

إذا كنت مهتمًا بإصدار حديث من النشيد، فقم بإلقاء نظرة على المستودع الجديد.

ملخص

يقوم anthem بترجمة برامج ASP (في لغة الإدخال الخاصة بـ clingo ) إلى لغة مثبتات النظرية من الدرجة الأولى مثل Prover9.

الاستخدام

للتحقق من أن البرنامج ينفذ إحدى المواصفات، قم باستدعاء anthem باستخدام أمر verify-program :

 $ النشيد التحقق من البرنامج <ملف البرنامج> <ملف المواصفات>...

لاحظ أنه قد يتم تحديد ملفات مواصفات متعددة. وهذا مفيد لفصل المفاهيم والبديهيات عن الافتراضات والمواصفات.

يمكن إعادة إنتاج مثال حساب أرضية الجذر التربيعي لرقم على النحو التالي:

 أمثلة لبرنامج التحقق من النشيد $/example-2.{lp,spec,lemmas}

تدوين الأقواس هو اختصار Bash لـ

 $ النشيد أمثلة التحقق من البرنامج/example-2.lp أمثلة/example-2.spec أمثلة/example-2.lemmas

افتراضيًا، يقوم anthem بإكمال كلارك للصيغ المترجمة، ويكتشف المتغيرات الصحيحة، ويبسط الإخراج من خلال تطبيق العديد من قواعد التحويل الأساسية.

يمكن إيقاف خطوات المعالجة هذه باستخدام الخيارات --no-complete و --no-simplify و --no-detect-integers .

مبنى

تم بناء anthem باستخدام سلسلة أدوات cargo الخاصة بـ Rust. بعد تثبيت Rust، يمكن بناء anthem على النحو التالي:

 استنساخ $ git https://github.com/potassco/anthem.git
$ مؤتمر نزع السلاح النشيد
بناء البضائع $ - الإصدار

سيكون ثنائي anthem متاحًا بعد ذلك في الدليل target/release/ . وبدلاً من ذلك، يمكن استدعاء anthem باستخدام cargo على النحو التالي:

 تشغيل البضائع $ - التحقق من البرنامج <ملف البرنامج> <ملف المواصفات>...

المساهمين

• باتريك لونه