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

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

للتوضيح ، سنقسم التحقق إلى التحقق من الشفرة (CV) والتحقق من التصميم (DV) وبنفس الطريقة نقسم المواصفات إلى CS و DS. لا يتم استخدام هذه المصطلحات بشكل شائع في مجتمع FM الواسع. لنبدأ باستخدام CS و CV ، ثم انتقل إلى DS و DV.

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

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

أخيرًا ، إخلاء المسئولية: لست مؤرخًا محترفًا ، وعلى الرغم من أنني حاولت التحقق من المعلومات بعناية ، فقد تكون هناك أخطاء في المقالة. بالإضافة إلى ذلك ، أنا متخصص في المواصفات الرسمية (DS و DV) ، لذلك هناك فرصة أكبر للخطأ عندما أتحدث عن التحقق من الكود. إذا رأيت ، اكتب لي ، فسأقوم بتصحيحه (وأحد الأشياء الأخرى: كسب المال من الندوات على TLA + وسبائك ، لذلك أنا متحيز جدًا تجاه هذه اللغات ؛ أحاول أن أكون موضوعيًا قدر الإمكان ، لكنك تفهم: التحيز هو التحيز).

البرمجة الرسمية

الحصول على المواصفات

قبل إثبات صحة الكود ، تحتاج إلى الحصول على معيار الحقيقة. هذا يعني بعض المواصفات لما يجب أن يفعله الكود. يجب أن نعرف على وجه اليقين أن النتيجة تطابق المواصفات. لا يكفي أن نقول إن القائمة "مرتبة": لا نعرف ما الذي نرتبه ، والمعايير التي نستخدمها ، وحتى ما نعنيه بـ "الفرز". بدلاً من ذلك ، يمكننا القول: " l فرز قائمة الأعداد الصحيحة l بترتيب تصاعدي لأي مؤشرين i و j ، إذا i < j ، ثم l[i] <= l[j] ."

تنقسم مواصفات الكود إلى ثلاثة أنواع رئيسية:

1. الأول هو كتابة بيانات مستقلة عن الكود. نكتب وظيفة الفرز لدينا ، وفي ملف منفصل نكتب نظرية "هذا يعيد قوائم مرتبة". هذا هو أقدم أشكال المواصفات ، لكن لا يزال إيزابيل و ACL2 يعملان بهذه الطريقة (تم اختراع ML خصيصًا للمساعدة في كتابة هذه المواصفات).
   
2. ينفذ الثاني المواصفات في التعليمات البرمجية في شكل ما قبل وما بعده ، والبيانات ، والمتغيرات. يمكنك إضافة شرط لاحق إلى الوظيفة "أن قيمة الإرجاع هي قائمة مرتبة." تم إضفاء الطابع الرسمي على المواصفات القائمة على المطالبات باعتبارها منطق هور . ظهرت لأول مرة في لغة البرمجة Euclid في أوائل السبعينيات (ليس من الواضح من بدأ استخدامها أولاً: Euclid أو SPV ، ولكن على حد علمي ، تم تقديم Euclid إلى الجمهور من قبل). يُسمى هذا النمط أيضًا برمجة العقود - الشكل الأكثر شيوعًا للتحقق في الصناعة الحديثة (هنا ، تُستخدم العقود كمواصفات رمز).
   
3. وأخيرا ، هناك أنظمة النوع. بواسطة مراسلات كاري - هوارد ، يمكن ترميز أي نظرية أو دليل رياضي كنوع تابع. سوف نحدد نوع القوائم التي تم فرزها ونعلن النوع [Int] -> Sorted [Int] لهذه الوظيفة.

على Let's Prove Leftpad ، يمكنك رؤية كيف يبدو. HOL4 و Isabelle هما مثالان جيدان على مواصفات "النظرية المستقلة" ، SPARK و Dafny هي مواصفات "البيان المتداخل" ، و Coq و Agda هما "النوع التابع".

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

أي المواصفات صحيحة؟

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

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

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

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

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

ولكن كل هذا لا علاقة له بالتحقق. عندما يكون لديك مواصفات ، لا يزال عليك إثبات أن الكود يطابقه.

دليل المواصفات

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

1. الخيار الأساسي : إذا أضفت عنصرًا واحدًا إلى القائمة الفارغة ، فسيكون العنصر الوحيد ، لذلك سيتم فرزه.
   
2. إذا كانت لدينا قائمة مرتبة بعناصر k وأضفت عنصرًا واحدًا ، فسنقوم بإدراج العنصر بحيث يكون بعد كل الأرقام الأصغر وقبل جميع الأرقام الكبيرة. هذا يعني أن القائمة ما زالت مرتبة.
   
3. عن طريق الاستقراء ، فرز الفرز سيتم فرز القائمة بأكملها.

من الواضح ، في الواقع ، سيبدو الدليل أكثر صرامة ، لكن هذه فكرة عامة. استخدم Dijkstra وآخرون هذا الأسلوب لإثبات صحة العديد من الخوارزميات ، بما في ذلك العديد من أساسيات التزامن. هذا هو أيضًا الأسلوب الذي ترتبط به كلمات Knuth : "احذر من الأخطاء في هذا الرمز ؛ لقد أثبتت فقط أنها كانت صحيحة ، لكنني لم أبدأها ". يمكنك تدمير دليل رياضي بسهولة حتى لا يلاحظه أحد. وفقًا لبعض التقديرات ، يحتوي حوالي 20٪ من الأدلة الرياضية المنشورة على أخطاء. لدى بيتر جوتمان مقال ممتاز عن الأدلة على صحة برنامج مثير للسخرية ، حيث يسقط على الفور الكثير من الشفرات "المختبرة" إذا قمت بتشغيلها.

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

مما يؤدي إلى المشكلة التالية.

الأدلة يصعب الحصول عليها

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

خذ نفس المثال الفرز الإدراج حيث طبقنا الحث. سوف يفهم أي عالم الرياضيات على الفور ما هو الحث ، وكيف يعمل بشكل عام ، وكيف يعمل في هذه الحالة. ولكن في برنامج لإثبات النظريات كل شيء يحتاج إلى إضفاء طابع رسمي صارم. وينطبق الشيء نفسه مع إثبات التناقض ، وإثبات من خلال المواجهة ، وما إلى ذلك. بالإضافة إلى ذلك ، يجب إضفاء الطابع الرسمي على جميع الافتراضات ، حتى تلك التي لا يزعج معظم علماء الرياضيات بالإثبات. على سبيل المثال ، a + (b + c) = (a + b) + c . برنامج التحقق من النظريات المسبقة لا يعلم أن هذا صحيح. عليك إما إثبات ذلك (صعب) ، أو إعلانه كحقيقة وفقًا لقانون الإضافة (خطير) ، أو شراء مكتبة للنظريات من شخص سبق أن أثبت أنه (مكلف). تنافست برامج إثبات النظريات المبكرة في عدد من التكتيكات المضمنة والمكتبات النظرية ذات الصلة. قدم أحد برامج SPADE الأولى على نطاق واسع المكتبة الحسابية الكاملة باعتبارها الميزة الرئيسية.

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

• الرياضيات
  
• علوم الحاسوب
  
• المنطقة التي تعمل فيها: المجمعون ، الأجهزة ، إلخ ؛
  
• الفروق الدقيقة في برنامجك وتخصصك ؛
  
• الفروق الدقيقة للبرنامج لإثبات النظريات التي تستخدمها ، والتي في حد ذاتها تخصص كامل.

والأسوأ من ذلك أن العصي الخاصة بالكمبيوتر وضعت في عجلات. تذكر ، قلت أنه كان من الخطير افتراض قانون الجمع من الجمع؟ بعض اللغات لا تمتثل له. على سبيل المثال ، في C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 هو INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) ، وهو أمر لا يمكن اكتشافه. بافتراض إضافة نقابي في C ++ ، سيكون دليلك غير صحيح ، وسيتم كسر الكود. يجب عليك إما تجنب هذا البيان أو إثبات أن الفائض لن يحدث أبدًا لشظيتك الخاصة.

يمكنك أن تقول أن الإضافة غير المحددة هي خطأ ، لكنك تحتاج إلى استخدام لغة مع أعداد صحيحة غير مرتبطة. لكن معظم اللغات لديها ميزات محددة تتداخل مع الأدلة. خذ الكود التالي:

 a = true; b = false; f(a); assert a; 

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

يواجه القائمون بعمليات التحقق الرسمية معضلة: كلما كانت اللغة أكثر تعبيرًا ، زادت صعوبة إثبات شيء ما. ولكن كلما كانت اللغة أقل تعبيرًا ، زادت صعوبة الكتابة عليها. كانت لغات العمل الرسمية الأولى مجموعات فرعية محدودة للغاية من اللغات الأكثر تعبيراً: كانت ACL2 مجموعة فرعية من Lisp ، وكانت Euclid مجموعة فرعية من Pascal ، وما إلى ذلك. ولم يثبت أي مما ناقشناه حتى الآن برامج حقيقية ، فهذه مجرد محاولات للتوجه لكتابة الأدلة.

الأدلة صعبة. لكن الأمر أصبح أسهل. يضيف الباحثون في هذا المجال الأساليب البحثية الجديدة ، ومكتبات النظريات ، والمكونات التي تم اختبارها مسبقًا ، وما إلى ذلك. كما يساعد التقدم التقني أيضًا: أجهزة الكمبيوتر الأسرع ، وأسرع عملية البحث.

SMT الثورة

كان أحد الابتكارات في منتصف العقد الأول من القرن العشرين إدراج حلول SMT في برامج لإثبات النظريات. بشكل عام ، يمكن لمحلل SMT أن يحول (بعض) النظريات الرياضية إلى مشاكل في التقييد. هذا يحول مهمة إبداعية إلى مهمة حسابية. قد لا تزال بحاجة إلى تزويدها بمشكلات متوسطة (عصير الليمون) كخطوات في النظرية ، ولكن هذا أفضل من إثبات كل شيء بنفسك. ظهرت حلول SMT الأولى حوالي عام 2004 ، أولاً كمشاريع أكاديمية. بعد ذلك بعامين ، أصدرت Microsoft Research Z3 ، وهو محلل SMT جاهز للاستخدام. كانت الميزة الكبيرة لـ Z3 هي أنه أصبح أكثر ملاءمة للاستخدام من SMTs الأخرى ، التي ، بصراحة ، لم تقل شيئًا تقريبًا. استخدمها Microsoft Research داخليًا للمساعدة في إثبات خصائص kernel Windows ، لذلك لم تكن مقصورة على الحد الأدنى من UX.

ضرب SMT مجتمع FM تحت التنفس لأنه جعل فجأة العديد من الأدلة البسيطة تافهة وسمحت لها بالتعامل مع مشاكل معقدة للغاية. وهكذا ، يمكن للناس أن يعملوا بلغات أكثر تعبيرا ، حيث بدأت الآن حل مشاكل البيانات التعبيرية. كان التقدم المذهل واضحًا في مشروع IronFleet : باستخدام أفضل حلول SMT ولغة تحقق متقدمة ، تمكنت Microsoft من كتابة 5000 سطر من كود Dafny الذي تم إثباته في 3.7 سنوات من العمل فقط! هذه سرعة سريعة بشكل لا يصدق: ما يصل إلى أربعة أسطر كاملة يوميًا (ملاحظة: السجل السابق ينتمي إلى seL4 ، والذي قام مطوروه بكتابة سطرين يوميًا في C.

الأدلة صعبة.

لماذا هذا مطلوب؟

حان الوقت للتراجع والسؤال: "ما هي النقطة؟" نحن نحاول إثبات أن بعض البرامج يلبي بعض المواصفات. الصواب هو المدى. هناك جزءان للتحقق: مدى صحة موضوعية البرنامج الخاص بك ومدى التحقق من صحة بعناية. من الواضح ، كلما كان التحقق أكثر ، كان ذلك أفضل ، ولكن التحقق يستحق الوقت والمال. إذا كان لدينا العديد من القيود (الأداء ، الوقت اللازم للتسويق ، التكلفة ، إلخ) ، فإن التحقق الكامل ليس بالضرورة الخيار الأفضل. ثم يطرح السؤال ، ما هو الحد الأدنى للتحقق الذي نحتاجه وما يكلفه. في معظم الحالات ، على سبيل المثال ، يكون تصحيح 90٪ أو 95٪ أو 99٪ كافيًا لك. ربما يجب عليك قضاء بعض الوقت في تحسين الواجهة ، بدلاً من التحقق من النسبة المتبقية البالغة 1٪؟

ثم السؤال: "هل الفحص بنسبة 90/95/99 ٪ أرخص بكثير من 100 ٪؟" الجواب نعم. من المريح تمامًا القول بأن قاعدة الشفرة ، التي قمنا باختبارها وكتابتها جيدًا ، صحيحة بشكل أساسي باستثناء بعض التصحيحات في الإنتاج ، وحتى نكتب أكثر من أربعة أسطر من الرموز يوميًا. في الواقع ، كان من الممكن منع الغالبية العظمى من الأعطال في الأنظمة الموزعة عن طريق إجراء اختبار أكثر شمولًا قليلاً. إنها مجرد امتداد للاختبارات ، ناهيك عن الاختبار المذهل أو الاختبار المعتمد على الملكية أو الاختبار النموذجي. يمكنك الحصول على نتيجة رائعة حقا مع هذه الحيل البسيطة دون الحاجة إلى الحصول على دليل كامل.

ماذا لو كانت الكتابة والاختبار لا توفر التحقق الكافي؟ لا يزال التبديل أسهل من 90٪ إلى 99٪ من 99٪ إلى 100٪. كما ذكرنا سابقًا ، فإن Cleanroom عبارة عن ممارسة مطورة تتضمن وثائق شاملة وتحليلًا دقيقًا للتيار ومراجعة شاملة للشفرة. لا دليل ، لا تحقق رسمي ، ولا حتى اختبار وحدة. لكن غرف الأبحاث المنظمة بشكل جيد تقلل من كثافة العيوب إلى أقل من خطأ واحد لكل 1000 سطر من الشفرة في الإنتاج (ملاحظة: أرقام من دراسة ستافلي في برنامج Toward Zero-Defect Programming > لكن دائمًا ما تكون متشككًا وتحقق من المصدر ). لا يؤدي برنامج غرف الأبحاث إلى إبطاء وتيرة التطوير ، وبالتأكيد يذهب أسرع من 4 خطوط في اليوم. و Cleanroom نفسها هي مجرد واحدة من العديد من أساليب تطوير البرامج الموثوقة للغاية والتي هي في منتصف الطريق بين التطوير العادي والتحقق من الكود. لا تحتاج إلى التحقق الكامل لكتابة برنامج جيد أو حتى الكمال تقريبا. في بعض الأحيان يكون ذلك ضروريًا ، لكن بالنسبة إلى معظم الصناعات ، يكون هذا مضيعة للمال.

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

التحقق الجزئي من الكود

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

المشكلة هي إمكانية الوصول .تم تصميم معظم اللغات إما للتحقق الكامل ، أو لا تدعمها على الإطلاق. في الحالة الأولى ، تفوت العديد من الميزات الجيدة من لغات أكثر تعبيراً ، وفي الحالة الثانية ، تحتاج إلى وسيلة لإثبات الأشياء بلغة معادية للمفهوم نفسه. لهذا السبب ، تركز معظم الدراسات حول التحقق الجزئي على عدة لغات ذات أولوية عالية ، مثل C و Java. يعمل الكثير منها مع مجموعات فرعية محدودة من اللغات. على سبيل المثال ، SPARK هي مجموعة فرعية محدودة من Ada ، لذلك يمكنك كتابة رمز SPARK الحرج والتفاعل مع كود Ada الأقل أهمية. ولكن معظم هذه اللغات هي مكانة جميلة.

في أغلب الأحيان ، يتم تضمين أنواع معينة من التحقق في البنية الأساسية للغات. أنظمة التصنيف المستخدمة في الإنتاج هي نوع شائع: قد لا تعرف أن الذيل دائمًا ما يعود إلى الذيل ، لكنك تعرف تمامًا نوعه [a] -> [a]. هناك أيضًا أمثلة مثل Rust مع أمان مثبت في الذاكرة و Pony مع إثبات للأمان مع استثناءات. إنهم مختلفون قليلاً عن SPARK و Frama-C من حيث أنه يمكنهم إجراء اختبارات جزئية فقط . وعادة ما يتم تطويرها من قبل خبراء في لغات البرمجة ، وليس خبراء في الطرق الرسمية: هناك الكثير من القواسم المشتركة بين التخصصات ، لكنها ليست متطابقة. ربما هذا هو السبب في أن لغات مثل Rust و Haskell مناسبة حقًا للاستخدام العملي.

مواصفات التصميم

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

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

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

• هل كل الرسائل مسجلة أم كل الرسائل التي تدخل النظام ؟ يتم تسجيل الرسائل مرة واحدة أو مضمونة مرة واحدة؟
  
• كيف يتم إرسال الرسائل؟ هل هذا هو الدور؟ هل تقوم القناة بتسليمها مرة واحدة فقط؟ هل كل شيء على ما يرام مع التسليم؟
  
• ? , ? «» , ?
  
• , ? ?
  
• ? « » ?
  
• GDPR?
  
• .

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

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

ربما كان أول DL كامل VDM حوالي عام 1972. منذ ذلك الحين ، رأينا مجموعة كبيرة ومتنوعة من لغات المواصفات المختلفة. تعد مساحة DL أكثر تنوعًا وتجزيءًا من لغات التحقق من الكود (CVL). تحدث تقريبًا ، اخترع الناس DL كوسيلة لتحقيق غاية ، و CVL كهدف في حد ذاته. نظرًا لأنها تتأثر بشدة بمناطق المشكلات المحددة ، تنفذ DL جميع أنواع الأفكار والدلالات. فيما يلي نظرة عامة موجزة جدًا على بعض من DLs الأولى:

اللغة	منطقة النمذجة	يعني
Z	متطلبات العمل	الجبر العلائقي
Promela		CSP
SDL		-

نظرًا لأن DLs يتم إنشاؤها عادةً لحل مشكلات محددة ، فإن معظمها لديها تطبيقان أو ثلاثة تطبيقات على الأقل. وكقاعدة عامة ، فإن النتائج إيجابية للغاية. يقول الممارسون إن DL توفر فهمًا للمشاكل ويجعل إيجاد الحلول أسهل. لفترة طويلة ، كان البطل الرئيسي هو Praxis (الآن Altran) ، الذي طبق "الإصلاح حسب التصميم" - مزيج من Z- الإنشاءات ورمز SPARK - لإنشاء أنظمة أمان مهمة. توفر المواصفات الوقت والمال لأنك لن تجد أخطاء التصميم في مرحلة متأخرة من المشروع.

جربت Pamela Zave شركة Alloy واكتشف خللًا أساسيًا في Chord ، أحد طاولات التجزئة الرئيسية الموزعة. يبدأ AWS في العثور على أخطاء حرجة من 35 خطوةعن طريق كتابة مواصفات TLA +. في تجربتي ، عندما يحاول الناس كتابة المواصفات ، سيصبحون قريبًا معجبين بهذا العمل.

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

لحسن الحظ ، يعد هذا أيضًا مهمًا للغاية للعديد من المحددات ، لذلك يعد التحقق من التصميم مجالًا كبيرًا من الأبحاث.

نموذج تحقق

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

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

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

عيب كبير آخر - انفجار في فضاء دول (انفجار فضاء الحالة). تخيل أن لديك ثلاث عمليات ، تتكون كل منها من أربع خطوات متتالية ، ويمكنها تغيير الخطوات بأي طريقة. إذا لم يؤثروا على سلوك بعضهم البعض ، فسيظهر بعد ذلك(4*3)! / (4!)^3 = 34 650عمليات الإعدام المحتملة (السلوكيات). إذا كان لكل عملية واحدة من خمس حالات مبدئية ، فإن العدد الإجمالي للسلوكيات يرتفع إلى 4300000. والتحقق من النماذج يجب أن تتأكد من أنها جميعًا تتصرف بشكل جيد. وهذا شريطة ألا يتفاعلوا مع بعضهم البعض! إذا بدأوا في القيام بذلك ، فسوف تنمو مساحة الولاية بشكل أسرع. يعتبر الانفجار التوافقي المشكلة الرئيسية لاختبار النماذج ، ولا يزال هناك الكثير من العمل الذي يتعين القيام به لحل هذه المشكلة.

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

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

مشكلة مواصفات التصميم

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

هذا يرجع إلى حد كبير إلى حقيقة أن التصميم ليس رمز . في معظم DLs ، لا توجد طريقة تلقائية لإنشاء الكود ، ولا توجد طريقة لأخذ الكود الموجود والتحقق منه مقابل التصميم (ملاحظة: يُطلق على توليد الكود من المواصفات التوليف ؛ لمعرفة الاتجاه ، راجع عمل Nadya Polikarpova ؛ إثبات أن الكود يطابق المواصفات (أو المواصفات تتوافق مع مواصفات أخرى) ويسمىتوضيح : بحث نشط يجري في كلا الاتجاهين).

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

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

لكن بالضبط لدى كل مجتمع منهجي مثل هذه الشكاوى التي أعرفها: يشكو أنصار TDD من أن المبرمجين لا يرغبون في تجربة TDD ، ويشكو عشاق Haskell من أن المبرمجين لا يفكرون في الكتابة الثابتة ، وما إلى ذلك.

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

من الصعب للغاية جعل الناس قلقين بشأن ما لم يفعلوه حتى الآن ، حتى لو أدركوا الفوائد.

ملخص

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

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

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