لغة نمذجة جافا

📅 آخر تحديث: ٢١ يوليو ٢٠٢٦
✍️ نُشر في: ٢١ يوليو ٢٠٢٦
الموسوعة الحرة

لغة نمذجة جافا ( JML ) هي لغة مواصفات لبرامج جافا ، تستخدم شروطًا مسبقة ولاحقة وثوابت على نمط هوار ، وتتبع نموذج التصميم التعاقدي . تُكتب المواصفات كتعليقات توضيحية في جافا لملفات المصدر، وبالتالي يمكن تجميعها باستخدام أي مُجمِّع جافا .

تساعد أدوات التحقق المختلفة، مثل مدقق تأكيدات وقت التشغيل ومدقق الثوابت الموسع ( ESC/Java )، في عملية التطوير.

ملخص

لغة JML هي لغة مواصفات سلوكية لواجهات وحدات جافا. توفر JML دلالات لوصف سلوك وحدة جافا بشكل رسمي، مما يمنع أي لبس فيما يتعلق بنوايا مصممي الوحدات. تستوحي JML أفكارها من لغات Eiffel و Larch وحساب التحسين ، بهدف توفير دلالات رسمية دقيقة مع الحفاظ على سهولة استخدامها لأي مبرمج جافا. تتوفر أدوات متنوعة تستخدم مواصفات JML السلوكية. ولأن المواصفات يمكن كتابتها كتعليقات توضيحية في ملفات برامج جافا، أو تخزينها في ملفات مواصفات منفصلة، ​​يمكن تجميع وحدات جافا التي تحتوي على مواصفات JML دون تغيير باستخدام أي مُجمِّع جافا.

بناء الجملة

تُضاف مواصفات JML إلى كود Java على شكل تعليقات توضيحية. تُفسَّر تعليقات Java على أنها تعليقات JML توضيحية عندما تبدأ بعلامة @. أي، التعليقات التي تأتي على الشكل التالي:

//@ <مواصفات JML>

أو

/*@ <مواصفات JML> @*/

توفر صيغة JML الأساسية الكلمات المفتاحية التالية

requires
يحدد شرطًا مسبقًا للطريقة التي تليها .
ensures
يُحدد شرطًا لاحقًا على الطريقة التي تليها.
signals
يحدد شرطًا لاحقًا لوقت طرح استثناء معين بواسطة الطريقة التي تليها.
signals_only
يحدد هذا ما هي الاستثناءات التي يمكن طرحها عندما يتحقق الشرط المسبق المحدد.
assignable
يحدد هذا الخيار الحقول التي يُسمح بتعيينها بواسطة الطريقة التالية.
pure
يُعلن هذا عن أن الدالة خالية من الآثار الجانبية (مثل الدالة `true` assignable \nothing، ولكنها قد تُطلق استثناءات أيضًا). علاوة على ذلك، من المفترض أن تنتهي الدالة النقية دائمًا إما بشكل طبيعي أو تُطلق استثناءً.
invariant
يُعرّف خاصية ثابتة للفئة .
loop_invariant
يُعرّف هذا الأمر ثابتًا للحلقة.
also
يجمع بين حالات المواصفات ويمكنه أيضًا أن يعلن أن طريقة ما ترث المواصفات من أنواعها الفائقة.
assert
يُعرّف تأكيد JML .
spec_public
يُعلن عن متغير محمي أو خاص كمتغير عام لأغراض التحديد.

توفر لغة JML الأساسية أيضًا التعبيرات التالية

\result
معرّف لقيمة الإرجاع للطريقة التالية.
\old(<expression>)
مُعدِّل للإشارة إلى قيمة المتغير <expression>في وقت الدخول إلى طريقة ما.
(\forall <decl>; <range-exp>; <body-exp>)
المُكمِّم العالمي .
(\exists <decl>; <range-exp>; <body-exp>)
المُكمِّم الوجودي .
a ==> b
aيشير إلىb
a <== b
aيُستدل على ذلك من خلالb
a <==> b
aإذا وفقط إذاb

بالإضافة إلى صيغة جافا القياسية للمعاملات المنطقية "و" و"أو" و"ليس". تتمتع تعليقات JML أيضًا بإمكانية الوصول إلى كائنات جافا، وأساليب الكائنات، والمعاملات التي تقع ضمن نطاق الأسلوب الذي يتم التعليق عليه، والتي تتمتع برؤية مناسبة. يتم دمج هذه العناصر لتوفير مواصفات رسمية لخصائص الفئات والحقول والأساليب. على سبيل المثال، قد يبدو مثال مُعلَّق عليه لفئة مصرفية بسيطة كما يلي:

public class BankingExample { public static final int MAX_BALANCE = 1000 ; private /*@ spec_public @*/ int balance ; private /*@ spec_public @*/ boolean isLocked = false ; //@ public invariant balance >= 0 && balance <= MAX_BALANCE; //@ assignable balance; //@ ensures balance == 0; public BankingExample () { this . balance = 0 ; } //@ requires 0 < amount && amount + balance < MAX_BALANCE; //@ assignable balance; //@ ensures balance == \old(balance) + amount; public void credit ( final int amount ) { this . balance += amount ; } //@ requires 0 < amount && amount <= balance; //@ assignable balance; //@ ensures balance == \old(balance) - amount; public void debit ( final int amount ) { this . balance -= amount ; } //@ ensures isLocked == true; public void lockAccount () { this . isLocked = true ; } //@ requires !isLocked; //@ ensures \result == balance; //@ also //@ requires isLocked; //@ signals_only BankingException; public /*@ pure @*/ int getBalance () throws BankingException { if ( ! this . isLocked ) { return this . balance ; } else { throw new BankingException (); } } }

تتوفر الوثائق الكاملة لبنية لغة JML في دليل مرجع JML .

دعم الأدوات

توفر مجموعة متنوعة من الأدوات وظائف تعتمد على تعليقات JML. توفر أدوات JML الخاصة بجامعة ولاية أيوا مُجمِّعًا للتحقق من التأكيدات يحولjmlc تعليقات JML إلى تأكيدات وقت التشغيل، ومولدًا للوثائق jmldocيُنتج وثائق Javadoc مُعززة بمعلومات إضافية من تعليقات JML، ومولدًا لاختبارات الوحدة jmlunitيُنشئ رمز اختبار JUnit من تعليقات JML.

تعمل مجموعات مستقلة على تطوير أدوات تستخدم تعليقات JML التوضيحية. وتشمل هذه الأدوات ما يلي:

  • ESC/Java2، وهو مدقق ثابت موسع يستخدم تعليقات JML لإجراء فحص ثابت أكثر صرامة مما هو ممكن بطريقة أخرى.
  • يُعلن OpenJML نفسه خليفة ESC/Java2.
  • تم أرشفة Daikon في 11-12-2005 على Wayback Machine ، وهو مولد ثابت ديناميكي.
  • KeY ، الذي يوفر برنامجًا مفتوح المصدر لإثبات النظريات مع واجهة أمامية JML ومكون إضافي لـ Eclipse ( تحرير JML ) مع دعم لتلوين بناء جملة JML.
  • تم أرشفة Krakatoa في 2009-05-08 في Wayback Machine ، وهي أداة تحقق ثابتة تعتمد على منصة التحقق Why وتستخدم مساعد إثبات Rocq .
  • JMLEclipse ، وهو مكون إضافي لبيئة التطوير المتكاملة Eclipse مع دعم لبنية JML وواجهات لأدوات متنوعة تستخدم تعليقات JML.
  • Sireum/Kiasan ، محلل ثابت قائم على التنفيذ الرمزي يدعم JML كلغة عقود.
  • JMLUnit ، أداة لإنشاء ملفات لتشغيل اختبارات JUnit على ملفات Java المشروحة بـ JML.
  • TACO ، أداة تحليل برامج مفتوحة المصدر تقوم بفحص توافق برنامج Java بشكل ثابت مع مواصفات لغة نمذجة Java الخاصة به.

مراجع

  • غاري تي. ليفنز ويونسيك تشون. التصميم التعاقدي باستخدام لغة JML ؛ دليل تعليمي للمسودة.
  • غاري تي. ليفنز ، وألبرت إل. بيكر، وكلايد روبي. JML: تدوين للتصميم التفصيلي ؛ في حاييم كيلوف، وبرنهارد رومبي ، وإيان سيموندز (محررون)، المواصفات السلوكية للشركات والأنظمة ، كلوير، 1999، الفصل 12، الصفحات 175-188.
  • غاري تي. ليفنز ، وإريك بول، وكورتيس كليفتون، ويونسيك تشيون، وكلايد روبي، وديفيد كوك، وبيتر مولر، وجوزيف كينيري، وباتريس شالين، ودانيال إم. زيمرمان. دليل مرجعي لـ JML (مسودة)، سبتمبر 2009. HTML
  • ماريك هويسمان ، فولفغانغ أهرندت، دانييل برونز، ومارتن هنتشل. المواصفات الرسمية مع JML . 2014. تحميل (CC-BY-NC-ND)