مُثبِّت نظرية Z3

مُثبِّت نظرية Z3

المؤلف(ون) الأصلي(ون)	أبحاث مايكروسوفت
المطور(ون)	مايكروسوفت
الإصدار الأولي	2012 ؛ منذ 12 سنة ( 2012 )
إصدار مستقر	4.13.3 [1]  / 11 أكتوبر 2024 ؛ منذ 44 يومًا ( 11 أكتوبر 2024 )
مستودع	github.com/Z3Prover/z3
مكتوب في	سي++
نظام التشغيل	ويندوز ، فري بي إس دي ، لينكس ( ديبيان ، أوبونتو )، ماك أو إس
منصة	IA-32 ، x86-64 ، WebAssembly ، arm64
يكتب	مُثبت النظرية
رخصة	رخصة معهد ماساتشوستس للتكنولوجيا
موقع إلكتروني	github.com/Z3Prover

Z3 ، المعروف أيضًا باسم Z3 Theorem Prover ، هو مُحلل نظريات قابلية الرضا (SMT) الذي طورته شركة Microsoft . ^[2]

تم تطوير Z3 في مجموعة أبحاث هندسة البرمجيات (RiSE) في Microsoft Research Redmond ويستهدف حل المشكلات التي تنشأ في التحقق من صحة البرامج وتحليل البرامج . يدعم Z3 العمليات الحسابية ومتجهات البت ذات الحجم الثابت والمصفوفات الامتدادية وأنواع البيانات والوظائف غير المفسرة والكميات . تطبيقاته الرئيسية هي الفحص الثابت الممتد وتوليد حالات الاختبار وتجريد المسندات . ^{[ بحاجة لمصدر ]}

تم طرح Z3 مفتوح المصدر في بداية عام 2015. ^[3] تم ترخيص الكود المصدر بموجب ترخيص MIT واستضافته على GitHub . ^[4] يمكن بناء الحل باستخدام Visual Studio أو ملف makefile أو باستخدام CMake ويعمل على أنظمة Windows و FreeBSD و Linux و macOS .

تنسيق الإدخال الافتراضي لـ Z3 هو SMTLIB2 . كما أنه يدعم رسميًا الارتباطات للعديد من لغات البرمجة ، بما في ذلك C و C++ و Python و. NET و Java و OCaml . ^[5]

في هذا المثال، يتم التحقق من تأكيدات المنطق القياسي باستخدام الدوال لتمثيل المقترحين a وb. يتحقق البرنامج النصي Z3 التالي لمعرفة ما إذا كان : ${\displaystyle {\overline {a\land b}}\equiv {\overline {a}}\lor {\overline {b}}}$

(أعلن-متعة أ () Bool)
(أعلن-متعة ب () Bool)
(أكد (ليس (= (ليس (و ab)) (أو (ليس أ) (ليس ب)))))
(التحقق-الجلسة)

نتيجة:

غير مشبع

لاحظ أن النص يؤكد نفي اقتراح الفائدة. النتيجة غير المشبعة تعني أن الاقتراح المنفي غير قابل للإشباع، وبالتالي إثبات النتيجة المرجوة ( قانون دي مورجان ).

يحل البرنامج النصي التالي المعادلتين المعطيتين، ويجد القيم المناسبة للمتغيرين a وb:

(إعلان ثابت لـ Int)
(إعلان ثابت ب Int)
(أكد (= (+ ab) 20))
(أكد (= (+ أ (* 2 ب)) 10))
(التحقق-الجلسة)
(الحصول على النموذج)

نتيجة:

قعد
(نموذج
  (تعريف-متعة ب () Int
    -10)
  (تعريف-متعة أ () Int
    30)
)

في عام 2015، حصلت Z3 على جائزة Programming Languages ​​Software Award من ACM SIGPLAN . ^{[6] [7]} في عام 2018، حصلت Z3 على جائزة Test of Time Award من المؤتمرات الأوروبية المشتركة حول نظرية وممارسة البرمجيات (ETAPS). ^[8] حصل الباحثان في Microsoft نيكولاي بيورنر وليوناردو دي مورا على جائزة Herbrand لعام 2019 للمساهمات المتميزة في التفكير الآلي تقديراً لعملهما في تطوير إثبات النظريات باستخدام Z3. ^{[9] [10]}

• التحقق الرسمي

• ليوناردو دي مورا؛ نيكولاي بيورنر (2008). "Z3: حل فعال لـ SMT". أدوات وخوارزميات لبناء وتحليل الأنظمة . 4963 : 337-340.
• السحر الداخلي وراء إثبات نظرية Z3

• الموقع الرسمي
• ملعب Z3 على الإنترنت