اختبارات أو أنواع

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

متى يجب استخدام الاختبارات ومتى؟ ما هي المعلومات والضمانات التي نتلقاها في مقابل جهودنا لكتابتها؟

سوف نلقي نظرة على مثال بسيط ومفتوش قليلاً تم التعبير عنه في Python و C و Haskell و Idris. سنرى أيضًا ما يمكن قوله حول التطبيق دون أي معرفة إضافية به ، في كل حالة.

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

مواصفة

واسمحوا قائمة وبعض المعطى. يجب عليك إرجاع فهرس هذه القيمة في القائمة أو الإشارة إلى أن هذه القيمة ليست في القائمة.

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

الثعبان

 def x(y, z): # 10000    

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

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

تحليل

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

• الوثائق
  
  • ✗ نحن نعرف السلوك المتوقع
    ليس لدينا ما نخبرنا به عن سلوك هذه الوظيفة. أنت تكره جدتك. انت وحش.
• الضمانات
  
  • ✓ أمن الذاكرة
    Python هي لغة جمع القمامة التي تزيل هذا القلق منا. "على أي حال ، حسب علمي ، لا شيء يمنعك من سحب المكتبات غير الآمنة أو C FFI داخل هذه الوظيفة."

بيثون مع الاختبارات

 def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None 

نحن نعلم الآن أن وظيفتنا تعمل ، وإذا كان العنصر مفقودًا ، فالنتيجة هي بلا؟

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

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

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

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

تحليل

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

• الوثائق
  
  • ✓ لدينا مثال للاستخدام
  • ✓ نحن نعرف بعض فئات القيم التي سيتم معالجتها بشكل صحيح
  • ✗ نحن نعرف جميع أنواع القيم التي سيتم معالجتها بشكل صحيح
    ليست لدينا قيود على أنواع الوسائط ، لذلك على الرغم من وجود أمثلة لما يمكن أن تتعامل به الوظيفة ، لا نعرف الأنواع التي لم يتم اختبارها.
  • ✗ نحن نعرف السلوك المتوقع
    "صاحب المقال الأصلي الذي تم وضع علامة هنا ، سوف أسمح لنفسي بوضع صليب ، بالنظر إلى التعليق أعلاه"
• مواصفة
  
  • ✓ يعمل في حالة واحدة على الأقل
  • returned الفهرس المرتجع هو دائما فهرس صالح
  • returned يشير المؤشر المرتجع دائمًا إلى قيمة مناسبة
  • item إرجاع العنصر المفقود دائمًا بلا / Nothing
• الأخطاء الشائعة
  
  • ✗ لا توجد أخطاء مطبعية أو أسماء غير صحيحة
    يمكن أن يساعد التحليل الثابت ، ولكن بما أن Python هي لغة ديناميكية لها القدرة على تجاوز أشياء مختلفة في وقت التشغيل ، لا يمكننا أبدًا إثبات عدم وجود أخطاء.
    على وجه الخصوص ، قد يكون من الصعب جدًا أو المستحيل تحديد ما إذا كان اسم الطريقة صحيحًا ، نظرًا لأن صلاحية استدعاء الأسلوب تعتمد على نوع وقت تشغيل الكائن الذي تم إجراء المكالمة عليه.
  • ✗ لا شيء غير متوقع
  • ✗ يتم التعامل مع حالة الخطأ دائمًا
    في تجربتي ، يعد هذا أحد أكثر مصادر الأخطاء شيوعًا: في المثال الخاص بنا ، None تُرجع الدالة None في حالة وجود عنصر مفقود ، ولكن الرمز الذي يستخدم هذه الوظيفة يمكن أن يفترض ، على سبيل المثال ، أنه سيعود دائمًا برقم. بالإضافة إلى ذلك ، يمكن أن يؤدي هذا أيضًا إلى استثناء غير معالج.
• الضمانات
  
  • ✓ أمن الذاكرة
  • cannot لا يمكن استدعاء الوظيفة بنوع خاطئ
  • ✗ لا توجد آثار جانبية
  • ✗ لا استثناءات
  • ✗ لا توجد أخطاء
  • ✗ لا دورات دائمة

هاسكل

 xyz = -- 10000   

إذا كنت غير معتاد على بناء الجملة: هذا هو تعريف الدالة x مع المعلمات y و z . في Haskell ، يمكنك حذف الأنواع ، حيث سيتم استنتاجها من التطبيق - بدون استخدام ، بالطبع ، يمكنك استخدام ميزات متقدمة مختلفة من الملحقات الحديثة لنظام الكتابة⟧.

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

تحليل

من الواضح أنه لا يمكننا استخلاص الكثير من الاستنتاجات هنا ، ولكن فيما يلي بعض النقاط التي يجب ملاحظتها:

• الوثائق
  
  • ✗ نحن نعرف السلوك المتوقع
• الأخطاء الشائعة
  
  • ✓ لا توجد أخطاء مطبعية أو أسماء غير صحيحة
    منذ Haskell هي لغة مترجمة ، يجب حل جميع الأسماء في وقت الترجمة. البرنامج ببساطة لن يتم ترجمة إذا كان هناك هذا الخطأ.
  • ✓ لا شيء غير متوقع
    هاسكل فقط لا يملك أي قيمة. تم حل المشكلة!
• الضمانات
  
  • ✓ أمن الذاكرة
  • cannot لا يمكن استدعاء الوظيفة بنوع خاطئ
  • ✓ لا توجد آثار جانبية غير متوقعة
    "لم يشير مؤلف المقال الأصلي إلى هذا العنصر ، لكنني سأسمح لنفسي بالإشارة إلى أنه في حالة وجود آثار جانبية ، فإن النوع المستنتج من هذه الوظيفة سيشير إلى وجودها ، حتى يعرف رمز الاتصال عن قدراتها."

تحديد نوع هاسكل

 x :: Eq a => [a] -> a -> Maybe Int xyz = -- ... 

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

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

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

تحليل

• الوثائق
  
  • ✓ نحن نعرف السلوك المتوقع
  • ✗ لدينا مثال للاستخدام
  • ✓ نحن نعرف بعض فئات القيم التي سيتم معالجتها بشكل صحيح
  • ✓ نحن نعرف جميع أنواع القيم التي سيتم معالجتها بشكل صحيح
• مواصفة
  
  • ✗ يعمل في حالة واحدة على الأقل.
    مع عدم وجود اختبارات أو أدلة ، لا نعرف ما إذا كانت وظيفتنا تعمل على الإطلاق كما نتوقع!
  • returned الفهرس المرتجع هو دائما فهرس صالح.
  • returned يشير المؤشر المرتجع دائمًا إلى قيمة مناسبة.
  • missing إرجاع العنصر المفقود دائمًا بلا / Nothing .
• الأخطاء الشائعة
  
  • ✓ لا توجد أخطاء مطبعية أو أسماء غير صحيحة
  • ✓ لا شيء غير متوقع
  • ✓ يتم التعامل مع حالة الخطأ دائمًا
    إذا Nothing تُرجع الدالة Nothing ، فإن نظام الكتابة يتأكد من معالجة هذه الحالة بشكل صحيح بواسطة رمز الاتصال. بالطبع ، يمكن تجاهل هذه الحالة ، ولكن يجب القيام بذلك بشكل صريح.
• الضمانات
  
  • ✓ أمن الذاكرة
  • cannot لا يمكن استدعاء الوظيفة بنوع خاطئ
  • ✓ لا توجد آثار جانبية
  • ✗ لا استثناءات
    أشارك الاستثناءات والأخطاء ، معتقدًا أنه بعد الاستثناءات ، من الممكن استردادها ، وبعد الأخطاء (على سبيل المثال ، وظائف محددة جزئيًا) - لا.
    بالنسبة للجزء الأكبر ، يتم وصف الاستثناءات في أنواع (على سبيل المثال ، في IO monad). بطريقة جيدة ، يجب أن نعرف أن الوظيفة لن تتسبب في استثناء ، فقط على أساس نوعه. ومع ذلك ، يكسر Haskell هذا التوقع من خلال السماح بالاستثناءات من الكود الخالص .
    "بالإضافة إلى ذلك ، تجدر الإشارة إلى أنه في Haskell ، يتم أيضًا عرض أخطاء مثل استدعاء وظائف محددة جزئيًا بشكل غير صحيح كاستثناءات يمكن اكتشافها ومعالجتها ، وبالتالي فإن الفرق بين الفئتين أقل وضوحًا قليلاً."
  • ✗ لا توجد أخطاء
    لا يزال بإمكاننا استخدام وظائف محددة جزئيًا ، على سبيل المثال ، القسمة على صفر.
  • ✗ لا دورات دائمة

هاسكل مع الاختبارات

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

على سبيل المثال:

 not :: Bool -> Bool not x = ... 

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

في الواقع ، هذا ليس صحيحًا تمامًا أيضًا في حالة هاسكل: في كل نوع من أنواع هاسكل ، هناك أيضًا قيمة ⊥ (والتي يمكن الحصول عليها على أنها undefined أو error أو بمعنى ما العودية اللامتناهية) ، لكن هاسكليست يغمضون أعينهم بشكل تقليدي ويعتقدون أن إنه غير موجود.

القراءة اللامنهجية: لا يوجد سوى أربعة بلايين عوامة - لذا اختبرهم جميعًا!

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

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

C

 /* C    ,    int */ int x(int *y, size_t n, int z) { /* 10000    */ } 

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

في مثالنا ، لا نعرف ما ستعود الوظيفة إذا لم يتم العثور على العنصر. سيتعين علينا الاعتماد على التقليد أو على الوثائق (على سبيل المثال ، في هذه الحالة قد يكون -1 ).

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

 /*   ,   out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000    */ } 

تحليل
نظام الكتابة في حد ذاته لا يعطينا الكثير من الضمانات. بالطبع ، نحصل على بعض المعلومات من هذه الأنواع ، ولكن فقط قم بمقارنتها بحالة Haskell.

إدريس

 x : Eq x => List x -> x -> Maybe Int xyz = ... 

هذه الوظيفة من نفس النوع كما في حالة هاسكل. ومع ذلك ، مع نظام الكتابة الأكثر تعبيرا ، يمكننا تحقيق المزيد. يمكن اختيار أنواع الحديث عن التنفيذ.

 %default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ... 

يمكن قراءة هذا النوع كـ "أعطني قائمة بالحجم n وبعض القيمة ، وسأرجع لك إما برقم أقل من n أو Nothing ." هذا يضمن أن تقوم الدالة بإرجاع فهرس من الواضح أنه لا يتجاوز الحدود.

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

تحليل

• مواصفة
  
  • ✗ يعمل في حالة واحدة على الأقل.
  • returned الفهرس المرتجع هو دائما الفهرس الصحيح
  • returned يشير المؤشر المرتجع دائمًا إلى قيمة مناسبة
  • item إرجاع العنصر المفقود دائمًا بلا / Nothing
• الضمانات
  
  • ✓ أمن الذاكرة
  • cannot لا يمكن استدعاء الوظيفة بنوع خاطئ
  • ✓ لا توجد آثار جانبية
  • ✗ لا استثناءات
  • ✓ لا توجد أخطاء
  • ✓ لا دورات دائمة

إدريس مع الاختبارات

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

 ex : x [1, 2, 3] 2 = Just 1 ex = Refl 

تحتوي هذه الوظيفة على نوع غريب نوعا ما x [1, 2, 3] 2 = Just 1 . يعني هذا النوع أنه في حالة إجراء فحص ناجح للنوع ، يجب أن يثبت typer أن x [1, 2, 3] 2 تساوي هيكلياً Just 1 . this في هذه الحالة ، يكون الدليل تافهًا ، حيث يكفي أن يقوم الشاحن بتطبيع الشروط على جانبي علامة المساواة ، والتي سيتم إجراؤها في وقت محدد بسبب إجمالي جميع الوظائف المستخدمة ، والتي سوف تؤدي إلى نتيجة فريدة بسبب Church-Rosser. بعد ذلك ، يمكن للمرء استخدام الانعكاسية للمساواة ، وهو ما Refl

في الواقع ، لقد كتبنا اختبار مستوى النوع.

إدريس مع الأدلة

لاستكمال التحليل ، يمكننا استخدام القوة الكاملة للأنواع التابعة وإثبات تطبيقنا (نظرًا لأن الأنواع التابعة في Idris تعادل نظامًا منطقيًا يتضمن منطقًا بناءً من الدرجة الأولى).

على وجه الخصوص ، يمكننا إثبات الخصائص التي لم يكن من الممكن الوصول إليها من قبل:

 --      Eq  DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... --    ,       `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ... 

يمكن قراءة findIndexOk كـ "لأي نوع a بحيث يكون لديه مقارنة قابلة DecEq ( DecEq ) له DecEq ، لأي متجه y لعناصر النوع a أي طول n وأي قيمة z النوع a : if xyz بإرجاع الفهرس i ، فإن هذا الفهرس الأكاذيب z ، ولكن إذا Nothing تعيد xyz Nothing ، فلا يوجد مثل هذا العنصر في المتجه على الإطلاق. "

"من المثير للاهتمام أن مؤلف المقال الأصلي يعطي نوعًا أضعف قليلاً من النوع المذكور أعلاه."

الآن لدينا كل شيء القبض! ما هي العيوب؟ حسنًا ، يمكن أن تكون كتابة كل هذه الأدلة صعبة للغاية.

مقارنة

رأي

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

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