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