23 سبتمبر 2025·8 دقيقة
أفكار توني هواري عن الصحة: من المنطق إلى شيفرة آمنة
تعرف كيف شكلت أفكار توني هواري — من منطق هواري وQuicksort إلى عقلية السلامة — تقنيات عملية لكتابة ومراجعة برمجيات صحيحة.
تعرف كيف شكلت أفكار توني هواري — من منطق هواري وQuicksort إلى عقلية السلامة — تقنيات عملية لكتابة ومراجعة برمجيات صحيحة.
عندما يقول الناس إن البرنامج "صحيح"، فهم غالبًا يقصدون: «شغّلته عدة مرات والمخرجات بدت صحيحة». هذا إشارة مفيدة — لكنها ليست الصحة. ببساطة، الصحة تعني أن البرنامج يفي بمواصفته: لكل مدخل مسموح به، ينتج النتيجة المطلوبة ويحترم أية قواعد حول تغيّر الحالة، التوقيت، والأخطاء.
المشكلة أن «يفي بالمواصفة» أصعب مما يبدو.
أولاً، المواصفات غالبًا غامضة. قد تقول متطلبات المنتج "رتب القائمة"، لكن هل هذا يعني ترتيبًا مستقرًا؟ ماذا عن القيم المكررة، القوائم الفارغة، أو العناصر غير العددية؟ إن لم تذكر المواصفة، سيفترض الناس أشياء مختلفة.
ثانيًا، حالات الحافة ليست نادرة — هي فقط تُختبر أقل تكرارًا. القيم الفارغة، الفائض، حدود off-by-one، تتابعات المستخدم غير الاعتيادية، وفشل خارجي غير متوقع يمكن أن يحوّل "يبدو أنه يعمل" إلى "فشل في الإنتاج".
ثالثًا، المتطلبات تتغير. قد يكون البرنامج صحيحًا بالنسبة لمواصفة الأمس وغير صحيح بالنسبة لمواصفة اليوم.
المساهمة الكبرى لتوني هواري لم تكن المطالبة بأن نبرهن على كل شيء دومًا. كانت الفكرة أننا يمكن أن نكون أكثر دقة بشأن ما يُفترض أن يفعله الكود — وأن نحاول العقلنة بطريقة منهجية.
في هذه المقالة سنتبع ثلاثة خيوط مترابطة:
معظم الفرق لن تكتب براهين رسمية كاملة. لكن حتى التفكير الجزئي «على طريقة البراهين» يمكن أن يجعل الأخطاء أسهل للاكتشاف، والمراجعات أكثر وضوحًا، والسلوك أوضح قبل تسليم الشيفرة.
توني هواري واحد من نادر علماء الحاسوب الذين لم تبق أعمالهم في الأوراق أو الفصول الدراسية فقط. تحرك بين الأكاديميا والصناعة، واهتم بسؤال عملي يواجهه كل فريق حتى اليوم: كيف نعرف أن البرنامج يفعل ما نظنه — خصوصًا عندما تكون الرهانات عالية؟
تركز هذه المقالة على بعض أفكار هواري التي تظهر باستمرار في قواعد الشيفرة الحقيقية:
{P} C {Q}.لن تجد هنا رسمًا رياضيًا عميقًا، ولن نحاول برهنة Quicksort بطريقة يمكن لآلة التحقق منها بالكامل. الهدف هو الحفاظ على المفاهيم قابلة للوصول: بنية كافية لجعل تفكيرك أوضح، دون تحويل مراجعة الشيفرة إلى سيميتر أكاديمي.
أفكار هواري تترجم إلى قرارات عادية: ما الفرضيات التي تعتمدها دالة، ماذا تضمن للمنادين، ما الذي يجب أن يبقى صحيحًا أثناء نصف حلقة، وكيف تلاحظ تغييرات "قريبة من الصحيحة" أثناء المراجعات. حتى عندما لا تكتب {P} C {Q} صراحةً، التفكير بهذا الشكل يحسن واجهات برمجة التطبيقات والاختبارات وجودة المناقشات حول الشيفرة المعقدة.
رؤية هواري أكثر صرامة من "اجتاز بعض الأمثلة": الصحة عن الوفاء بوعد متفق عليه، لا عن المظهر الجيد على عينة صغيرة.
الأخطاء غالبًا تحدث عندما يتخطى الفرقون الخط الأوسط: يقفزون من المتطلبات مباشرةً إلى الشيفرة، مما يترك «الوعد» غامضًا.
هناك ادعاءان مختلفان غالبًا ما يُختلطان:
بالأنظمة الحقيقية، «عدم الانتهاء» يمكن أن يكون ضارًا مثل «الانتهاء بنتيجة خاطئة».
عبارات الصحة ليست عالمية؛ هي تعتمد على افتراضات حول:
الوضوح بشأن الافتراضات يحول "يعمل على جهازي" إلى شيء يمكن للآخرين تفسيره ومراجعته.
فكر في دالة sortedCopy(xs).
مواصفة مفيدة يمكن أن تكون: «تعيد قائمة جديدة ys بحيث (1) ys مرتبة تصاعديًا، و(2) ys تحتوي بالضبط على نفس عناصر xs (بنفس التكرارات)، و(3) xs لم تتغير.»
الآن "صحيح" يعني أن الشيفرة تفي بهذه النقاط الثلاث تحت الافتراضات المصرح بها — ليس فقط أن المخرجات بدت مرتبة في اختبار سريع.
منطق هواري طريقة للحديث عن الشيفرة بنفس الوضوح الذي ستستخدمه للتحدث عن عقد: إذا بدأت في حالة تحقق فيها افتراضات معينة، وشغّلت قطعة الشيفرة هذه، ستنتهي في حالة تحقق فيها ضمانات معينة.
الصياغة الأساسية هي مثل هور:
{precondition} program {postcondition}
الشرط المسبق يحدد ما يجب أن يكون صحيحًا قبل تشغيل قطعة الشيفرة. هذا ليس ما تأمل أن يكون صحيحًا؛ هو ما يحتاجه الكود ليعمل بشكل موثوق.
مثال: لنفترض دالة تُرجع متوسط رقمين بدون فحوصات فيضان.
a + b يساوي قيمة ضمن نوع العدد الصحيحavg = (a + b) / 2avg يساوي المتوسط الرياضي لـ a و bإن لم يتحقق الشرط المسبق (احتمال الفائض)، فالوعد في الشرط اللاحق لم يعد ينطبق. المثل يجبرك على قول ذلك بصراحة.
الشرط اللاحق يحدد ما سيكون صحيحًا بعد تشغيل الكود — بشرط أن الشرط المسبق تحقق. الشروط اللاحقة الجيدة ملموسة ويمكن التحقق منها. بدلًا من «النتيجة صالحة»، اذكر ماذا تعني «صالحة»: مرتبة، غير سالبة، ضمن النطاق، لم تتغير إلا حقول محددة، إلخ.
منطق هواري يتوسع من جمل بسيطة إلى شيفرة متعددة الخطوات:
x = x + 1 ما الحقائق الجديدة عن x؟\n- التسلسل («افعل هذا ثم ذلك») يربط الضمانات: إذا الخطوة 1 تؤسس شرطًا مسبقًا للخطوة 2، يصبح من الأسهل الوثوق بالكتلة بأكملها.الفكرة ليست رشق أقواس متعرجة في كل مكان، بل جعل النية قابلة للقراءة: افتراضات واضحة، نتائج واضحة، ومحادثات أقل من نوع "يبدو أنه يعمل" في المراجعات.
حاصل الحلقة هو تعبير صحيح قبل بدء الحلقة، يظل صحيحًا بعد كل تكرار، وما يزال صحيحًا عند انتهاء الحلقة. فكرة بسيطة بعائد كبير: تحل محل "يبدو أنه يعمل" بمطالبة يمكنك التحقق منها في كل خطوة.
بدون حاصل، المراجعة غالبًا ما تكون: «نمر عبر القائمة ونُصلح الأشياء تدريجيًا.» الحاصل يجبرك على الدقة: ما الذي أصبح صحيحًا الآن بالضبط، مع أن الحلقة لم تنته؟ بمجرد أن تصف ذلك بوضوح، تصبح أخطاء off-by-one والحالات المفقودة أسهل للاكتشاف، لأنها تظهر كلحظات يُكسر فيها الحاصل.
معظم الشيفرات اليومية يمكن أن تستفيد من بعض القوالب الموثوقة.
1) حدود / سلامة الفهارس
حافظ على الفهارس في نطاق آمن.
0 <= i <= nlow <= left <= right <= highهذا النوع من الحاصل رائع لمنع الوصول خارج النطاق ولجعل مبرهنة المصفوفات ملموسة.
2) عناصر معالجة مقابل غير معالجة
اقسم بياناتك إلى منطقة "منجزة" ومنطقة "لم تُنجز بعد".
a[0..i) تم فحصها."\n- "كل عنصر مُنقل إلى result يحقق شرط الفلترة."هذا يحول التقدّم الغامض إلى عقد واضح حول ما معنى "تمت معالجته".
3) بادئة مرتبة (أو بادئة مقسمة)
شائع في الفرز، الدمج، والتقسيم.
a[0..i) مرتبة."\n- "كل العناصر في a[0..i) هي <= pivot، وكل العناصر في a[j..n) هي >= pivot."حتى لو لم تكن المصفوفة كاملة مرتبة بعد، فقد حدّدت ما هو مرتّب بالفعل.
الصحة ليست فقط أن تكون صحيحًا؛ يجب أن تنتهي الحلقة أيضًا. طريقة بسيطة للإقناع هي تسمية مقياس (غالبًا ما يسمونه variant) يقلُّ كل تكرار ولا يمكنه الانخفاض إلى الأبد.
أمثلة:
n - i يتناقص بمقدار 1 كل مرة."\n- "عدد العناصر غير المعالجة يتناقص."\n
إن لم تجد مقياسًا يتناقص، فقد تكون أمام مخاطرة حقيقية: حلقة لا نهائية على بعض المدخلات.لـ Quicksort وعد بسيط: مع قطعة (شريحة) من الصفيف، أعد ترتيب عناصرها بحيث تكون في ترتيب غير تنازلي، دون فقد أو اختراع أي قيم. شكل الخوارزمية العام سهل الملخص:
إنه مثال ممتاز للتعليم لأن حجمه صغير بما يكفي ليبقى في الرأس، لكنه غني بما يكفي ليُظهر أين يفشل التفكير غير الرسمي. Quicksort الذي "يبدو أنه يعمل" على بعض الاختبارات العشوائية قد يكون خاطئًا بطرق تظهر فقط عند مدخلات أو حدود محددة.
قليل من القضايا يسبب معظم الأخطاء:
لإثبات الصحة بطريقة هواري عادةً تفصل البرهان إلى جزأين:
هذا الفصل يجعل العقلانية قابلة للإدارة: أصلح التقسيم، ثم ابن على ذلك صحة الفرز.
سرعة Quicksort تعتمد على روتين خدع صغير: التقسيم. إن كان التقسيم حتى بقليل خاطئ، يمكن أن يسيء Quicksort الترتيب، أو يدخل في حلقة لانهائية، أو يتحطم على حالات الحافة.
سنعمل بمخطط التقسيم الكلاسيكي لِـ Hoare (مؤشرين يتحركان إلى الداخل).
المدخل: شريحة من المصفوفة A[lo..hi] وقيمة pivot مختارة (غالبًا A[lo]).
المخرج: فهرس p بحيث:
A[lo..p] هو <= pivot\n- كل عنصر في A[p+1..hi] هو >= pivotلاحظ ما لا يُوعد: المحور لا يولد بالضرورة عند الموضع p، والعناصر المساوية للمحور قد تظهر على أي من الجانبين. هذا مقبول — Quicksort يحتاج فقط انقسامًا صحيحًا.
بينما يتقدم الخوارزم مؤشرين—i من اليسار وj من اليمين—التركيز الجيد يكون على ما هو «مؤمن» بالفعل. مجموعة حواصل عملية هي:
A[lo..i-1] هي <= pivot (الجانب الأيسر نظيف)\n- كل العناصر في A[j+1..hi] هي >= pivot (الجانب الأيمن نظيف)\n- كل شيء في A[i..j] غير مصنَّف (لا زال للتحقق)عندما نجد A[i] >= pivot وA[j] <= pivot، فإن تبديلهما يحافظ على هذه الحواصل ويقصر الوسط غير المصنَّف.
i يتحرك إلى اليمين؛ يجب أن ينتهي التقسيم ويُعيد فهرسًا معقولًا.\n- كلها أكبر من المحور: j يتحرك إلى اليسار؛ نفس القلق بشأن النهاية.\n- الكثير من المتساوين: إن كانت المقارنات غير متسقة (< vs <=)، قد تتوقف المؤشرات. مخطط هواري يعتمد على قاعدة متسقة حتى يستمر التقدّم.\n- مرتبة أصلاً / مرتبة عكسياً: لا يجب أن يكسر العقدة، حتى لو تدهور الأداء.توجد مخططات تقسيم مختلفة (Lomuto، Hoare، التقسيم ثلاثي). المفتاح هو اختيار مخطط، بيان عقده، ومراجعة الشيفرة مقابل ذلك العقد باستمرار.
الثقة في العودية أسهل عندما تجيب عن سؤالين بوضوح: متى تتوقف؟ ولماذا كل خطوة صحيحة؟ التفكير على طريقة هواري يساعد لأنه يجبرك على بيان ما يجب أن يكون صحيحًا قبل الاستدعاء، وما سيكون صحيحًا بعد عودته.
الدالة العودية تحتاج على الأقل حالة أساس حيث لا تجري استدعاءات عودية إضافية وتظل تحقق النتيجة الموعودة.
للترتيب، حالة الأساس النموذجية هي "المصفوفات ذات الطول 0 أو 1 مرتبة بالفعل." هنا، "مرتبة" يجب أن تكون صريحة: لعلاقة ترتيب ≤، المصفوفة مرتبة إذا لكل فهرسين i < j، لدينا a[i] ≤ a[j]. (مسألة الحفاظ على ترتيب العناصر المتساوية تسمى الاستقرار؛ Quicksort عادة غير مستقر ما لم تصمم ليكون كذلك.)
كل خطوة عودية ينبغي أن تستدعي نفسها على مدخل أصغر بشكل صارم. هذا «التقلص» هو حجة النهاية: إذا الحجم ينخفض ولا يمكن أن ينخفض دون حد، فلا يمكن أن تستدعي إلى الأبد.
التقلص مهم أيضًا لسلامة المكدس. حتى الشيفرة الصحيحة قد تتعطل إذا عمق العودية كبير جدًا. في Quicksort، الانقسامات غير المتوازنة قد تنتج عمق عودية كبير. هذه حجة للنهاية وتذكير عملي للنظر في أسوأ عمق.
أسوأ حالة لـ Quicksort قد تصل إلى O(n²) عند الانقسامات غير المتوازنة، لكن هذا مسألة أداء — ليس فشل صحة. هدف العقلانية هنا: بافتراض أن خطوة التقسيم تحافظ على العناصر وتقسّمها بحسب المحور، فإن فرز النطاقات الأصغر عوديًا يعني أن النطاق كله يفي بتعريف الترتيب.
الاختبار والمنطق الأسلوبي للبراهين يسعيان لنفس الهدف — الثقة — لكن بوسائل مختلفة.
الاختبارات ممتازة لالتقاط أخطاء ملموسة: off-by-one، حالة هامشية مفقودة، تراجع. لكن مجموعة الاختبارات لا تستطيع إلا أن تُجَرِّب مساحة المدخلات. حتى "تغطية 100%" لا تعني "تم فحص كل السلوكيات"؛ عادةً تعني "تم تنفيذ كل الأسطر".
التفكير بأسلوب البرهان يبدأ من مواصفة ويسأل: إذا تحققت هذه الشروط المسبقة، هل الشيفرة دائمًا تحقق الشروط اللاحقة؟ عندما تفعل ذلك جيدًا، لا تكتشف فقط خطأً — بل يمكنك غالبًا استبعاد فئة كاملة من الأخطاء (مثل "الوصول للمصفوفة يبقى داخل النطاق" أو "الحلقة لا تكسر خاصية التقسيم").
المواصفة الواضحة هي مولد اختبارات.
إذا قالت شرطك اللاحق "المخرجات مرتبة وهي تبديل من المدخلات"، تحصل تلقائيًا على أفكار للاختبارات:
المواصفة تخبرك ماذا يعني "صحيح"، والاختبارات تتحقق ما إذا كانت الحقيقة تطابقه.
اختبارات الخاصيات تقع بين البراهين والأمثلة. بدل اختيار حالات قليلة يدويًا، تُصِف خصائص وتدع أداة تولّد كثيرًا من المدخلات.
للفرز، خاصيتان بسيطتان تعطيان فائدة كبيرة:
هذه الخصائص هي في الأساس شروط لاحقة مكتوبة كفحوصات قابلة للتنفيذ.
روتين خفيف يتدرج:
اجعل "مواصفة + ملاحظات عقلانية + اختبارات" جزءًا من قالب PR أو قائمة مراجعة المراجعة (انظر أيضًا /blog/code-review-checklist).
إذا كنت تستخدم سير عمل توليد الشيفرة من واجهة محادثة، تنطبق نفس الانضباط — وربما أكثر. في Koder.ai، على سبيل المثال، يمكنك البدء في وضع التخطيط لتثبيت الشروط المسبقة/اللاحقة قبل توليد أي شيفرة، ثم التكرار مع لقطات واسترجاع أثناء إضافة اختبارات خاصية. الأداة تسرع التنفيذ، لكن المواصفة تبقى ما يمنع "السرعة" من أن تصبح "هشة".
الصحة ليست فقط أن "البرنامج يعيد القيمة الصحيحة". تفكير السلامة يطرح سؤالًا مختلفًا: ما النتائج غير المقبولة، وكيف نمنعها — حتى عندما تكون الشيفرة مضغوطة، مستخدمة بشكل خاطئ، أو تفشل جزئيًا؟ عمليًا، السلامة هي الصحة مع نظام أولويات: بعض الفشل مزعج، وبعضه قد يسبب خسارة مالية، انتهاك خصوصية، أو ضررًا جسديًا.
الخطأ عيب في التصميم أو الشيفرة. الخطر هو حالة يمكن أن تؤدي إلى نتيجة غير مقبولة. خطأ واحد قد يكون ضارًا في سياق وغير مؤذي في آخر.
مثال: خطأ off-by-one في معرض صور قد يخطئ تسمية صورة؛ نفس الخطأ في حاسبة جرعات الأدوية قد يؤذي المريض. تفكير السلامة يجبرك على ربط سلوك الشيفرة بالعواقب، وليس فقط بالامتثال للمواصفة.
لا تحتاج إلى طرق رسمية ثقيلة للحصول على فوائد سلامة فورية. يمكن للفرق اعتماد ممارسات صغيرة وقابلة للتكرار:
هذه التقنيات تتوافق طبيعيًا مع تفكير هواري: تضع الشروط المسبقة صريحة (ما المدخلات المقبولة) وتضمن أن الشروط اللاحقة تتضمن خصائص السلامة (ما يجب ألا يحدث أبدًا).
الفحوص المخصصة للسلامة تكلف: زمن CPU، تعقيد، أو رفضات خاطئة أحيانًا.
تفكير السلامة أقل عن إثبات الأناقة وأكثر عن منع أوضاع الفشل التي لا يمكن تحملها.
مراجعات الشيفرة هي المكان الذي يدفع فيه التفكير في الصحة أسرع، لأنك يمكن أن تلتقط الافتراضات المفقودة قبل أن تصل الأخطاء للإنتاج. الحركة الأساسية لهواري — بيان ما يجب أن يكون صحيحًا قبل وما سيكون صحيحًا بعد — تتحول بسهولة إلى أسئلة للمراجع.
عندما تقرأ تغييرًا، حاول تأطير كل دالة رئيسية كوعد صغير:
عادة مراجعة بسيطة: إن لم تتمكن من قول الشروط المسبقة/اللاحقة في جملة واحدة، فربما تحتاج الشيفرة إلى هيكلة أوضح.
للدوال الخطرة أو المركزية، أضف تعليق عقد صغير فوق التوقيع. اجعلها ملموسة: المدخلات، المخرجات، التأثيرات الجانبية، والأخطاء.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
هذه التعليقات ليست براهين رسمية، لكنها تعطي المراجعين شيئًا محددًا للتحقق منه.
كن واضحًا بشكل إضافي عند مراجعة شيفرة تتعامل مع:
إن غيّر التغيير أيًا من هذه، اسأل: "ما هي الشروط المسبقة، وأين تُنفَّذ؟" و"ما الضمانات حتى عند الفشل؟"
التفكير الرسمي لا يعني تحويل كامل قاعدة الشيفرة إلى ورقة علمية. الهدف هو قضاء مزيد من اليقين في الأماكن التي تدفع فيها الفائدة: حيث "يبدو جيدًا في الاختبارات" لا يكفي.
ملائمة عندما يكون لديك وحدة صغيرة وحيوية يعتمد عليها كل شيء (التوثيق، قواعد الدفع، الصلاحيات، قواطع السلامة)، أو خوارزمية معقدة حيث أخطاء off-by-one تختبئ لشهور (التحليلات، جداول المواعيد، التجريدات المتزامنة، تحويلات البيانات ذات الحدود الكثيفة).
قاعدة مفيدة: إن كان الخطأ يمكن أن يسبب ضررًا حقيقيًا أو خسارة مالية كبيرة أو تلف بيانات صامت، فأنت تريد أكثر من مراجعة عادية + اختبارات.
بإمكانك الاختيار بين "خفيف" و"ثقيل"، وغالبًا أفضل النتائج تأتي من المزج:
قرّر عمق الرسمية بموازنة:\n\n- المخاطر: التأثير × الاحتمال. مخاطر أعلى تبرر ضمانات أقوى.\n- التكلفة: وقت تحديد المواصفة، البرهنة، والصيانة.\n- معدل التغيير: الشيفرة سريعة التغير أصعب للحفاظ عليها رسميًا؛ ثبّت الواجهات أولًا.\n- مهارات الفريق: ابدأ بالعقود والتحليل الثابت إذا كانت البراهين ستبطئ التسليم كثيرًا.
عمليًا، يمكنك أيضًا التعامل مع "الرسمية" كشيء تضيفه تدريجيًا: ابدأ بعقود وحواصل واضحة، ثم دع الأتمتة تحافظ عليها. لفرق تعمل بسرعة على Koder.ai — حيث توليد واجهات React، باكند Go، ومخطط Postgres قد يحدث في حلقة ضيقة — اللقطات/الاسترجاع وتصدير الشيفرة يجعل من الأسهل التكرار بسرعة مع إجبار على العقود عبر الاختبارات والتحليل الثابت في CI.
استخدم هذه كبوابة صغيرة "هل نحتاج أن نزيد الرسمية؟" في التخطيط أو مراجعة الشيفرة:
قراءات مقترحة: التصميم بالعقود، اختبارات الخاصيات، التحقق النموذجي لآلات الحالات، المحللات الثابتة للغتك، ومقدمة عن مساعدي الإثبات والمواصفات الرسمية.
الصحة تعني أن البرنامج يفي بمواصفة متفق عليها: لكل مدخل مسموح به وحالة نظام ذات صلة، ينتج المخرجات والآثار الجانبية المطلوبة ويتعامل مع الأخطاء كما وُعِد. عبارة «يبدو أنه يعمل» عادةً تعني أنك اختبرت بعض الأمثلة فقط، وليس فضاء المدخلات الكامل أو حالات الحدود الحساسة.
المتطلبات هي هدف العمل بلغة بسيطة («رتب القائمة للعرض»). المواصفة هي الوعد الدقيق والقابل للفحص («تعيد قائمة جديدة مرتبة تصاعدياً، تحتوي على نفس متعدد المجموعة من العناصر، والمدخلات تبقى دون تغيير»). التنفيذ هو الشيفرة. كثير من الأخطاء تحدث عندما يتخطى الفريق خطوة المواصفة ويذهب مباشرة من المتطلبات إلى التنفيذ بدون وعد قابل للفحص.
الصحة الجزئية: إذا عاد الكود، فالناتج صحيح.
الصحة الكلية: الكود يعيد النتيجة وفوق ذلك النتيجة صحيحة—إذًا النهاية جزء من المطالبة.
عملياً، الصحة الكلية مهمة كلما كان «التوقف إلى الأبد» فشلًا مرئيًا للمستخدم، أو تسربًا للمصادر، أو خطرًا على السلامة.
مثل هور {P} C {Q} يقرَأ كعقد:
P (ما قبل): ما يجب أن يكون صحيحاً قبل تشغيل CC: قطعة الشيفرةالشروط المسبقة هي ما يحتاجه الكود (مثلاً: «الفهارس ضمن النطاق»، «العناصر قابلة للمقارنة»، «المقفل محتجز»). إذا كان بالإمكان خرق شرط مسبق من قبل المستدعيين، إما:
إلا، تصبح الشروط اللاحقة مجرد تمنٍ.
حاصل الحلقة هو تعبير صحيح قبل بدء الحلقة، يظل صحيحًا بعد كل تكرار، وما يزال صحيحًا عندما تنتهي الحلقة. قوالب مفيدة:
0 <= i <= n)a[0..i) مرتبة)إن لم تستطع صياغة حاصل، فهذه إشارة أن الحلقة تفعل أكثر من اللازم أو أن الحدود غير واضحة.
تُسمِّي عادةً مقياسًا (متغيرًا) ينخفض في كل تكرار ولا يمكنه الانخفاض إلى مالانهاية، مثل:
n - i ينخفض بمقدار 1إذا لم تجد مقياسًا يتناقص، فقد اكتشفت خطر عدم النهاية الحقيقي (خصوصاً مع المكررات أو مؤشرات متوقفة).
في Quicksort، جزء التقسيم هو الروتين الصغير الذي يعتمد عليه كل شيء. إذا كان التقسيم خاطئًا قليلاً، قد تحصل على:
لذلك من المفيد بيان عقدة التقسيم صراحةً: ما يكون صحيحًا في الجانب الأيسر، وما يكون صحيحًا في الجانب الأيمن، وأن العناصر أعيد ترتيبها فقط (تبديل/تزاحم)، أي أنها لا تُفقد أو تُختلق.
التكرارات والقيم «المساوية للمحور» هي نقاط فشل شائعة. قواعد عملية:
i/j)إذا كانت التكرارات شائعة، فكّر في تقسيم ثلاثي لتقليل الأخطاء وعمق الاستدعاء العودي.
الاختبار يكشف أخطاء محددة؛ التفكير بأسلوب الإثبات يقضي على فئات كاملة من الأخطاء (سلامة الحدود، حفظ الحواصل، النهاية). سير عمل عملي هجين:
للمسح، الخاصيتان ذواتا القيمة العالية هما:
QCPلا تحتاج لكتابة الرموز في الشيفرة—استخدام البنية عملياً في المراجعات («افتراضات إلى الداخل، ضمانات إلى الخارج») هو الربح العملي.