التحقّق الصوري في البرمجيات التجارية: تقرير ميداني

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

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

التحفّظ هو النطاق. التحقّق من النظام كله كان سيكون عبثًا اقتصاديًا؛ التحقّق من المئتي سطر حيث يتحرك المال استغرق ثلاثة أسابيع وسدّد كلفته عند أول اكتشاف. هذا هو النمط الذي نوصي به الآن: الطرق الصورية كمِبضع، تُطبَّق تمامًا حيث الفشل غير محتمَل الكلفة.