sturdy

لم يعد يتم الحفاظ على نسخة Haskell من Sturdy. تم إعادة تنفيذ المشروع القوي في Scala وهو متاح على https://gitlab.rlp.net/plmz/sturdy.scala.

قوي

Sturdy هي مكتبة لإنشاء تحليلات ثابتة في Haskell. التحليلات الثابتة هي الأدوات التي تنتج معلومات حول برامج الكمبيوتر دون تشغيل البرنامج بالفعل. أمثلة على التحليلات الثابتة هي المدققون من النوع ، ومكتشفو الأخطاء (مثل Java FindBugs) ، وتحليلات للأمن (على سبيل المثال التحليلات) ، والتحليلات التي يتم استخدامها لتحسينات المترجمة.

يركز هذا المشروع على تحليلات سليمة ثابتة. التحليل الثابت هو سليم إذا تعكس نتائج التحليل سلوك وقت التشغيل الفعلي للبرنامج ويمكن للمستخدمين الاعتماد على النتائج. على سبيل المثال ، إذا كان التحليل الثابت المستخدم لتحسينات البروتشرات غير سليم ، فقد يغير التحسين دلالات البرنامج ، مما يؤدي إلى سلوك غير متوقع في وقت التشغيل. تحقيقًا لهذه الغاية ، يتبع Sturdy نظرية أدلة Soundness Conpositional للمترجمين الفوريين التجريديين والمكونات السليمة والقابلة لإعادة الاستخدام للتفسير التجريدي لتبسيط أدلة Sounds of Sounds of Static.

العوامل القوية تضع المترجم الملموس والمترجم التجريدي (التحليل الثابت) في مترجم عام . يتم تحديد المترجم المترجم العام بواسطة واجهات تحتوي على عمليات بدائية تصف دلالات اللغة ، مثل try ، catch ، finally للاستثناءات. ثم يقوم المترجم الملموس والتجريدي بتسهيل المترجم العام من خلال تنفيذ هذه الواجهات. لا تؤدي إعادة التنظيم هذه فقط إلى تفكيك المخاوف المختلفة في تنفيذ التحليل الثابت ، ولكن أيضًا يبسط إثبات السلامة. يمكن العثور على مزيد من التفاصيل في ورقة ICFP الخاصة بنا.

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

ابدء

للبناء ، قم بتثبيت أداة إنشاء المكدس وقم بتشغيل stack build من الدليل الجذر للمشروع.

يحتوي المشروع القوي حاليًا على المترجمين الفوريين الملموسة والتجريديين لللغات التالية:

• PCF ، لغة وظيفية عالية الترتيب
• بينما ، لغة ضرورية مع الشرطية وبين الحلقات
• مخطط ، لغة لغة وظيفية في عائلة LISP.
• Stratego ، لغة لتحويل البرامج
• Lambdajs ، تمثيل وسيطة لجافا سكريبت
• Jimple ، java bytecode مناسب للتحليل الثابت (العمل قيد التقدم)

لتشغيل اختبارات لغة معينة ، استخدم stack test sturdy-$(lang) ، على سبيل المثال ،

 stack test sturdy-pcf

المنشورات

خوارزميات FixPoint المستندة إلى Combinator للمترجمين التجريدين ذوي الخطوات الكبيرة
سفين كيديل ، سيباستيان أردويج ، توبياس هومبوش
المؤتمر الدولي للبرمجة الوظيفية (ICFP). ACM ، 2023. [PDF]

المترجمون التعريفي المجردة المعيارية للتجميع على الويب
كاثرينا براندل ، سيباستيان أردويغ ، سفين كيديل ، نيلز هانسن
المؤتمر الأوروبي حول البرمجة الموجهة نحو الكائن (ECOOP). ACM ، 2023. [PDF]

نهج منهجي للتفسير التجريدي لتحويلات البرنامج
سفين كيدل وسيباستيان أردويج.
التحقق ، فحص النموذج ، والتفسير التجريدي (VMCAI). سبرينغر ، 2020. [PDF]

مكونات سليمة وقابلة لإعادة الاستخدام للتفسير التجريدي
سفين كيدل وسيباستيان أردويج.
البرمجة الموجهة نحو الكائنات والأنظمة واللغات والتطبيقات (OOPSLA). ACM ، 2019 [PDF] [Talk]

أدلة سلامة التركيبة من المترجمين المجردين
سفين كيدل ، كاسبر باخ بولسن وسيباستيان أردويج.
المؤتمر الدولي للبرمجة الوظيفية (ICFP). ACM ، 2018 [PDF] [Talk]

شكر وتقدير

المشروع القوي هو جهد مشترك بين الأشخاص التاليين (بالترتيب الأبجدي):

Casper Bach Poulsen ، Jente Hidskes ، Matthijs Bijman ، Sarah Müller ، Sebastian Erdweg ، Sven Keidel ، Tobias Hombücher ، Wouter Raateland