key

مفتاح - برامج جافا الاستنتاجية

هذا المستودع هو موطن مفتاح Prover Interactive Theorem للتحقق الرسمي وتحليل برامج Java. يأتي المفتاح كتطبيق مستقل مستقل واجهة المستخدم الرسومية ، والذي يسمح لك بالتحقق من الصواب الوظيفي لبرامج Java فيما يتعلق بالمواصفات الرسمية التي تم صياغتها في لغة نمذجة Java JML. علاوة على ذلك ، يمكن أيضًا استخدام المفتاح كمكتبة على سبيل المثال لتنفيذ البرنامج الرمزي ، أو التفكير الأول من الدرجة الأولى ، أو توليد حالة الاختبار.

لمزيد من المعلومات ، راجع

• الصفحة الرئيسية الرئيسية
• الكتاب الرئيسي
• وثائق المطور الرئيسية
• قصص نجاح Key:
  • علة شديدة تم اكتشافها في روتين فرز JDK (TIMSORT) ،
  • التحقق من java.util.IdentityHashMap ،
  • جائزة Google لتحليل خطأ في LinkedList

الإصدار الحالي من المفتاح هو 2.12.2 ، مرخصة بموجب GPL V2.

لا تتردد في استخدام قوالب المشروع للبدء في استخدام المفتاح:

• لمشاريع التحقق
• باستخدام مكتبة
• باستخدام الواجهة الخلفية للتنفيذ الرمزي

متطلبات

• الأجهزة:> = 2 جيجابايت ذاكرة الوصول العشوائي
• نظام التشغيل: Linux/Unix ، MacOSX ، Windows
• جافا 17 أو الأحدث
• اختياريا ، يمكن للمفتاح الاستفادة من الثنائيات التالية:
  • SMT Solvers:
    • Z3
    • CVC5
    • CVC4
    • أميرة

محتوى المجلد الرئيسي

يوفر هذا المجلد مشروعًا يديره Gradle بعد تخطيط المجلد القياسي لـ Maven. هناك العديد من المشروعات الفرعية في هذا المجلد. بشكل عام ، يحتوي كل key.*/ المشروع الفرعي على مكون أساسي للمفتاح. المكونات الإضافية والاختيارية موجودة في keyext.*/ المجلدات. الملف build.gradle هو البرنامج النصي لبناء الجذر الذي يصف التبعيات ومهام البناء الشائعة لجميع المشروعات الفرعية.

key.util ، key.core و key.ui هي قاعدة المنتج "key prover". هناك حاجة إلى رعاية خاصة إذا كنت تخطط لإجراء تغييرات هنا.

تجميع وتشغيل المفتاح

على افتراض أنك في دليل ملف ReadMe هذا ، يمكنك إنشاء إصدار قابل للتشغيل وقابل للنشر مع أحد هذه الأوامر:

1. باستخدام ./gradlew key.ui:run يمكنك تشغيل واجهة المستخدم للمفتاح مباشرة من المستودع. استخدام ./gradlew key.ui:run --args='--experimental'

2. استخدام ./gradlew classes وبالمثل ، استخدم ./gradlew testClasses إذا كنت تريد أيضًا تجميع فئات اختبار Junit.

3. اختبار التثبيت الخاص بك مع ./gradlew test . كن على علم بأن هذا سيستغرق عادة عدة ساعات لإكماله. باستخدام ./gradlew testFast

   يمكنك تحديد حالة اختبار محددة مع وسيطة --tests . يسمح بحشود البرية.

   ./gradlew :key. < subproject > :test --tests " <class>.<method> "

   يمكنك تصحيح المفتاح بإضافة خيار-- --debug-jvm ، ثم إرفاق مصحح تصحيح في localhost:5005 .

4. يمكنك إنشاء جرة واحدة ، ويعرف أيضا باسم جرة الدهون ، من المفتاح مع

   ./gradlew :key.ui:shadowJar

   يتم إنشاء الملف في key.ui/build/libs/key-*-exe.jar .

5. يتم بناء التوزيع مع

   ./gradlew :key.ui:installDist :key.ui:distZip

   يمكن اختبار التوزيع عن طريق استدعاء key.ui/install/key/bin/key.ui ويتم ضربه في key.ui/build/distributions .

   يمنحك التوزيع إمكانية استخدام ملفات جرة واحدة.

تطوير المفتاح

• يتم تقييم الجودة تلقائيًا باستخدام Sonarqube في كل طلب سحب. يمكن فحص نتائج التقييمات (تمرير/فشل) في قسم الشيكات في العلاقات العامة.

  يتم الحفاظ على القواعد وبوابة الجودة بواسطة Alexander Weigl [email protected] حاليًا.

• يمكن العثور على مزيد من التوجيهات والوثائق للتطوير الرئيسي تحت المفاتيح.

القضايا وتقارير الأخطاء

• للحصول على تقارير الأخطاء ، يرجى استخدام تعقب المشكلات أو إرسال بريد إلى [email protected].

• للمناقشات ، قد ترغب في الاشتراك واستخدام القائمة البريدية [email protected] أو استخدام مناقشات github.

المساهمة في المفتاح

لا تتردد في تقديم طلبات السحب عبر GitHub. يتم تقييم طلبات السحب باستخدام الاختبارات التلقائية ، والتنسيق ، والفحص المدقق ، بالإضافة إلى مراجعة يدوية من قبل أحد المطورين. يمكن العثور على مزيد من الإرشادات والوثائق للتطوير الرئيسي تحت المفاتيح.

ملاحظة ترخيص

 This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
						Universität Koblenz-Landau, Germany
						and Chalmers University of Technology, Sweden
Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
						Technical University Darmstadt, Germany
						Chalmers University of Technology, Sweden

The KeY system is protected by the GNU General Public License.
See LICENSE.TXT for details.