formulog

الصيغة

TL ؛ DR: تحليل البرنامج المستند إلى SMT (المنفذين الرمزيين ، فصائهم نوع الصقل ، إلخ) بلغة تشبه DataLog المحسنة.

أثبتت Datalog أنها لغة مفيدة لتنفيذ مجموعة من تحليلات البرنامج ، لكن التحليلات التي تستخدم حل SMT لا يمكن كتابتها بسهولة في الإصدارات التقليدية من Datalog. يضع Formulog لملء هذه الفجوة عن طريق زيادة DataLog بطرق لبناء وسبب صيغ SMT ، بالإضافة إلى بعض البرمجة الوظيفية من الدرجة الأولى لجعل الحياة أسهل.

لماذا تكتب تحليلك المستند إلى SMT في الصيغة؟

1. من خلال الجمع بين البرمجة المنطقية ، والبرمجة الوظيفية ، وحل SMT ، يجعل الصيغة من الممكن تشفير العديد من التحليلات بشكل إعلاني على مستوى المواصفات الرياضية (على سبيل المثال ، قواعد الاستدلال) ، وإغلاق الفجوة بين المواصفات والتنفيذ --- وغالبًا ما تكشف عن الأخطاء في المواصفات!
2. هذا الترميز رفيع المستوى يجعل من الممكن لتطبيق تحسينات عالية المستوى على تحليلك ، مثل التوازي التلقائي والتقييم الموجهة للهدف.
3. بفضل برنامج التحويل البرمجي إلى الصيغة إلى soufflé ، يمكنك تلقائيًا إنشاء إصدار C ++ من التحليل الذي يعزز خوارزميات DataLog المحسنة للغاية وهياكل البيانات.

مهتم؟ لمزيد من المعلومات ، تحقق من مستندات Formulog (متوفرة أيضًا في دليل المستندات) ، بما في ذلك نصائح حول البدء ومرجع اللغة. للحصول على شعور بما ينطوي على بناء تحليل غير قائم على SMT في صيغة الصيغة ، تحقق من تعليمنا حول تنفيذ مدقق نوع التحسين في الصيغة.

المساهمة

المساهمات في هذا المشروع هي موضع ترحيب كبير! يرجى فتح مشكلة github ثم ربط طلب سحب إليها. يجب أن تكون طلبات السحب في تنسيق Google Java قبل دمجها. لإعادة تنسيق الكود الخاص بك ، قم بتشغيل mvn spotless:apply ؛ يمكنك أيضًا التحقق مما إذا كان الكود الخاص بك مطابقًا (بدون إعادة تنسيقه) عن طريق تشغيل mvn spotless:check .

مكتبات الترخيص ومكتبات الطرف الثالث

يتم إصدار Formulog بموجب ترخيص Apache 2.0.

يستخدم هذا المشروع مكتبات الطرف الثالث. يمكنك إنشاء قائمة بهذه المكتبات وتنزيل التراخيص المرتبطة بها مع هذا الأمر:

 mvn license:download-licenses

يمكن العثور على المحتوى الذي تم إنشاؤه في target/generated-resources/ الدليل.