تجارب مع استخدام السبائك في مشاريع العالم الحقيقي

Question

لقد كنت مهتمًا بالطرق الرسمية لبعض الوقت. لقد استخدمت طرقًا رسمية للتسبب في بعض المشاريع الفرعية المحددة للغاية لعدد قليل من المشاريع التي كنت أعمل عليها. لم أتمكن أبدًا من إقناع أعضاء الفريق الآخرين بتجربة نفس الشيء ناهيك عن تحديد مجال كامل بطريقة رسمية.

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

سأكون مهتمًا جدًا بسماع أي تجارب حقيقية قد تكون لدى الأشخاص مع استخدام السبائك في مشاريعك. هل تشعر أنه ساعدك في تصميم نموذج مجال أفضل؟ هل وجدت أخطاء في نموذج المجال الخاص بك أثناء التحقق؟ هل ستستخدمه مرة أخرى؟

Answer 1

نعم ، لقد استخدمت سبيكة وأبناء العم. لقد كانت سبيكة مفيدة للغاية في إقناعي بأن نماذجاتي لم تكن خاطئة بشكل كبير-أو بالأحرى ، تُظهر لي أين كانوا مخطئين وأدت إلى نتائج سخيفة. كانت الأدوات الأخرى الأكثر تحديدًا ، مثل Athena's Athena و Guttman و Ramsdell's CPSA أكثر فائدة في مجالاتهم الأضيق. ماذا تريد أن تسمع عنه أكثر؟

Answer 2

لقد استخدمت سبيكة في عدد قليل من المشاريع ووجدتها مفيدة ؛ في بعض هذه المشاريع ولكن ليس كل تلك المشاريع ، تمكنت من إقناع الآخرين المعنيين باستخدام سبيكة أيضًا ، أو على الأقل للعمل مع نماذج السبائك التي كتبتها. قد تكون هذه المشاريع أو لا تكون ما يدور في ذهنك في طلب مشاريع "العالم الحقيقي" ، لكنها بالتأكيد حدثت في العالم الحقيقي الذي أعمل فيه.

في عامي 2006 و 2007 ، قمت بإنشاء نموذج سبائك جزئي للمسودة التي تعمل في آنذاك من مواصفات W3C XPROC ؛ بقدر ما أستطيع أن أقول ، فإن معظم أعضاء مجموعة العمل لم يقرأوا الورقة التي كتبتها (على http://www.w3.org/xml/xproc/2006/12/alloy-models/models.html) ؛ قالوا "أوه ، لقد غيرنا هذا الجزء من المواصفات الأسبوع الماضي ، لذا فإن ما يقوله النموذج لم يعد ذا صلة". لكن الورقة تمكنت من إقناع محرر المواصفات بأن مستوى "المكون" التجريدي الموصوف في المسودة الأولى للمواصفات قد تم تحديده بشكل محزن ويحتاج إلى تحديد أو إسقاط بالكامل. لقد أسقطها ، مع (على ما أظن) نتائج جيدة لقابلية القراءة وسهولة الاستخدام للمواصفات.

في عام 2010 ، صنعت نموذج السبائك لنموذج بيانات XPath 1.0, والتي كشفت بعض مواطن الخلل في المواصفات. لم يكن رد فعل معظم الأطراف المهتمة (بما في ذلك مجموعة عمل W3C المسؤولة عن الحفاظ على مواصفات XPath 1.0) أمرًا مشجعًا.

استخدم مشروع بحثي الذي شاركت فيه سبيكة لنمذجة مجموعة MLCD تداخل ، وهي مجموعة من مستندات العينة والمعلومات ذات الصلة التي ننشئها (ارتباطات تشعبية مكبوتة عند إصرار SO) ؛ وجد نموذج السبائك بعض الأخطاء في تصميمنا الأولي لكتالوج كوربوس ، لذلك كان يستحق كل هذا الجهد.

وقد استخدمنا أيضًا سبيكة لإضفاء الطابع الرسمي على بعض أعمال النمذجة التي قمنا بها على طبيعة النسخ وعلى امتداد التمييز بين النوع/الرمز المميز لتوثيق بنية (لورقةنا ، ابحث عن وقائع Balisage 2010: مؤتمر الترميز). هذا يكمن قليلاً خارج مجال التطبيق المعتاد في Alloy ، لأنه لا علاقة له بتصميم البرمجيات ، ولكن قدرة Alloy على التحقق لنموذجنا.

للإجابة على أسئلتك المحددة: نعم ، ساعدتني Alloy في تحديد نماذج المجال المنظف ، ونعم ، لقد وجدت أخطاء ومواطن الخلل. غالبًا ما كانوا صغارًا ، للأسباب التي يشرحها دانييل جاكسون في كتابه تجريد البرمجيات: أولاً ، إذا كنت تستخدم النماذج أثناء التصميم ، فأنت تلتقط أخطاء مبكرًا ، متى كل شىء لا تزال صغيرة. والثاني (بكلمات جاكسون) ، "بعد فوات الأوان ، فإن معظم مشكلات تصميم البرامج تافهة."

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

Answer 3

إضافة متأخرة إلى هذا الموضوع ... قام Eunsuk Kang مؤخرًا بتطبيق سبيكة لإجراء تحليلات أمان من واجهات برمجة التطبيقات على الويب لبعض الشركات الناشئة (بعد العديد من تطبيقات السبائك في الأمان مثل Apurva's تحليل oauth وبارث وآخرون تحليل آليات الأمن القائمة على المتصفح ل CSRF وما إلى ذلك) ؛ تعمل باميلا زاف على تحليل مثير للإعجاب للترت, ، نظام تخزين نظير إلى الأقران ، وقد كتب مؤخرًا إصلاحًا إلى الخوارزمية الأصلية.