مواصفات الدقة الكلية هي أيضًا مواصفات صحة جزئية. يكون التصحيح الجزئي أضعف لأنه يحتاج إلى مساعدة إضافية من "إنهاء S" للوصول إلى الاستنتاج: R يحمل في الحالة النهائية.

للحصول على مواصفات صحة جزئية {Q} S {R} ، يمكنك الحصول على المعلومات التالية: بالنظر إلى حالة البداية التي ترضي Q ، S قد تنتهي أو لا. في حالة إنهاء S ، بعد تنفيذ S ، ستصل إلى حالة نهائية ترضي R. إذا لم يكن الأمر كذلك ، فإن R غير مجدية نظرًا لعدم وجود حالة نهائية.

فمثلا:

{س} == 10
بينما (ص! = 0):
    ص = ص - 1
س = 0
{س} == 0

إنها مواصفات صحة جزئية. إذا تمت تهيئة y مع رقم ما يساوي أو أكبر من 0 ، فسوف تنتهي S وبعد ذلك x هي 0. بينما إذا بدأت y برقم سالب ، فستتكرر S إلى الأبد وبما أنها لا تنتهي ، فلن تصل إلى حالة " بعد تنفيذ S '.

في الواقع ، يمكن أن يكون R أي شيء إذا كانت S حلقة ميتة. على سبيل المثال ، لأي سؤال وجواب:

{س}
احيانا صحيح):
    ص = ص - 1
{R}

هو دائما مواصفات صحة جزئية.

إذا كانت Q ليست قوية بما يكفي ، فلا يمكنك ضمان إنهاء S ، ناهيك عن سبب الحالة بعد إعدام S. في هذه الحالة ، يمكنك إضافة شرط يدويًا: إنهاء S. مع Q و ، يمكن أن يستمر المنطق.

بالنسبة لمواصفات الدقة الكاملة {Q} S {R} ، Q قوية بما يكفي لضمان إنهاء S ، بحيث يمكنك استنتاج أن S ستنتهي وترضي الحالة النهائية R.

فمثلا:

{x == 10}
بينما (س! = 0):
    س = س - 1
{x == 0}

هي مواصفات الصحيح الكلي.

راجع للشغل: لست متأكدًا مما إذا كانت الإجابة صحيحة لأن السؤال مصحوب بالسياسة الصحيحة. في حين أن التعريف الوارد في السؤال يبدو كما هو الحال في علوم الكمبيوتر.