تعتبر الطرق الرسمية وسيلة فعالة ، لكنها معقدة بشكل غير معقول لضمان موثوقية البرنامج. الأدوات المستخدمة لهذا تختلف اختلافا كبيرا عن تلك المألوفة للمبرمج. تمت كتابة هذه المقالة بهدف خفض عتبة إدخال مجموعة الأدوات هذه. سوف أستخدم نظام
فحص النماذج ليس لحل المهام التي تصاغ بصعوبة في مواصفات البرمجيات ، ولكن لحل لغز يمكن فهمه حتى لأطفال المدارس.
أنت في ممر مباشر مع سبع غرف في جانب واحد. في واحد منهم هو القط. في خطوة واحدة ، يمكنك النظر إلى إحدى الغرف ، إذا كان هناك قطة ، يتم القبض عليه. بمجرد إغلاق الباب ، سينتقل القطة إلى إحدى الغرف المجاورة إلى الغرفة التي كان فيها. المهمة هي للقبض على القط.
TLA + والمنطق الزمني
هناك العديد من الأدوات التي يمكن أن تحل هذه المشاكل. في كثير من الأحيان في مثل هذه الحالات ، يتم استخدام
حل SMT . كقاعدة عامة ، تستخدم مثل هذه الأنظمة المنطق الأصلي المعتاد والتعبير عن تسلسل الإجراءات أمر معقد للغاية (عليك استخدام شيء يشبه المصفوفة ، وهو ليس مناسبًا جدًا للعمل معه). يستخدم
TLA + المنطق الزمني ، والذي يسمح باستخدام حالة النظام في عبارة واحدة في الوقت الحالي وفي الخطوة التالية.
CatDistr' = CatDistr \ {n}
ينص هذا الشرط على أن مجموعة الغرف التي يمكن أن توجد فيها القطة بعد التحقق من الغرفة n تتزامن مع مجموعة الغرف التي تم أخذ n منها (إذا كانت القطة هناك ، يتم القبض عليه ولم يعد هناك ما يفعله).
في لغات البرمجة الحتمية ، يتوافق هذا تقريبًا مع تعيين قيمة جديدة للمتغير ، يتم حسابها من القيمة القديمة.
قليلا عن مجموعات
كما فهمت ، فإن موقع القط مصمم على شكل متغير مع مجموعة من جميع الغرف الممكنة ، وليس غرفة محددة ، كما سيكون في نظام المحاكاة. يعد استخدام مجموعة من القيم المحتملة بدلاً من قيمة محددة أسلوبًا شائع الاستخدام في الطرق الرسمية ، مما يسبب صعوبة للمبرمجين المبتدئين. لذلك ، اخترت مهمة يكون فيها استخدام المجموعات مناسبًا.
هيكل البرنامج في TLA +
في أبسط الحالات ، يتكون البرنامج من تصريحات وبيانات (تقديرات) تصف الحالة الأولية ، والعلاقة بين الحالة الحالية والحالة التالية ، والمتغير الذي يجب تنفيذه في جميع الحالات المتاحة. المسندات المساعدة قد تكون موجودة أيضا. يمكن أن تكون المعلمات المعلمات.
---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} =============================================================================
السطرين الأول والأخير هما ميزات بناء جملة إعلان الوحدة النمطية.
== تعني "المساواة بحكم التعريف" ، في حين أن
= = هي بالضبط المساواة في القيم المحسوبة للتعبيرات.
الأبواب هي نموذج ثابت ، وسوف تحتاج إلى تعيين في ملف التكوين.
CatDistr - توزيع القط في الغرف.
يتم إدخال متغير LastDoor ، آخر غرفة تم التحقق منها ، لسهولة إخراج البرنامج. بالنسبة للنماذج الكبيرة ، يمكن أن تؤدي هذه المتغيرات إلى إبطاء البرنامج بشكل كبير عن طريق زيادة عدد الحالات التي تم تحليلها (نظرًا لأن الحالة تحتوي الآن على سجل لكيفية ظهوره ، فإن الحالات نفسها التي تم إنشاؤها بطرق مختلفة ستكون مختلفة الآن).
يصف المسند الأولي الحالة الأولية (0..الأبواب هي مجموعة جميع الغرف). يصف OpenDoor (n) ما يحدث عندما تفتح الباب للغرفة n (في أسوأ الحالات ، القط ليس موجودًا - وإلا فقد وقعناه).
المسند التالي يبدو غريبا بعض الشيء - هناك مجال للنظر فيه. والحقيقة هي أن وجود شيء ما يعني أن TLA + لا تعرف أي مجال سنبحث فيه ، وبالتالي ، فسوف يتحقق من صحة المتغير في جميع الحالات.
سيكون أكثر وضوحا للكتابة
Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors)
ولكن بعد ذلك ، لن يعمل رمزنا إلا مع عدد محدد من الغرف ، ومن الأفضل جعله معاملات.
أخيرًا ، فإن CatWalk الثابت هو الكثير من الغرف التي قد لا تكون فيها القطة فارغة. انتهاك الثابت يعني أن القط تم القبض عليه ، أينما كان في الأصل. عند التحقق من المواصفات ، يعني انتهاك المتغير خطأً ، لكننا لا نستخدم الأداة للغرض المقصود منه و "الخطأ" الموجود يعني حل المشكلة.
التكوين النموذجي
CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk
كل شيء بسيط هنا - لقد أشرنا إلى عدد الغرف والشروط الأولية وشروط تغيير الحالة والمتغير قيد الاختبار.
تم إطلاق النموذج من سطر الأوامر
tlc2 -config cat.cfg cat.tla .
يحتوي TLA + على واجهة المستخدم الرسومية المتقدمة التي أطلقها فريق tla-toolbox. لسوء الحظ ، فهو لا يفهم ملفات .cfg وسوف تحتاج إلى تكوين معلمات الطراز من خلال القائمة.
استنتاج
في هذه المهمة ، تبين أن كل شيء بسيط للغاية. بطبيعة الحال ، فإن الحالات المهمة من الناحية العملية لتطبيق الأساليب الرسمية ستتطلب نماذج أكثر كثافة واستخدام العديد من المنشآت اللغوية. ولكني آمل أن يوفر حل هذه الألغاز طريقة بسيطة وغير مملة لتنفيذ الأساليب الرسمية في مشاريع العمل.
→ تم العثور على المهمة
هنافقط في حالة ، برنامج بسيط
للتحقق الحل التفاعلي . مواد
لدراسة TLA + . تم وصف نظام فحص نموذج آخر ، وهو سبيكة ،
هنا .