1. حدود الاختبار البرمجي وجدار عدم القابلية للحسم: لماذا لا يكفي اجتياز مليون اختبار؟

1.1 مقولة ديكسترا الخالدة والانفجار التوافقي لفضاء المدخلات

في عام 1969، وخلال مؤتمر حلف الناتو لهندسة البرمجيات، أطلق العالم الحائز على جائزة تورينغ إدسخر ديكسترا (Edsger W. Dijkstra) أشهر قاعدة في تاريخ علوم الحاسوب:

“Program testing can be used to show the presence of bugs, but never to show their absence!" (يمكن استخدام اختبار البرامج لإثبات وجود الأخطاء، لكن لا يمكن أبداً استخدامه لإثبات عدم وجودها!)

لنتأمل دالة بسيطة f(x, y) تستقبل عددين صحيحين بطول 64 بت (int64_t). إن إجمالي عدد أزواج المدخلات الممكنة هو:

حتى لو استخدمنا حاسوباً خارقاً ينفذ مليار ($10^9$) اختبار في الثانية الواحدة، فإن تجربة جميع المدخلات ستستغرق نحو $1.08 \times 10^{22}$ سنة — أي حوالي 780 مليار ضعف عمر الكون! ومع إضافة الذاكرة الديناميكية وتداخل الخيوط المتزامنة (Interleaving)، يقفز عدد مسارات التنفيذ إلى ما لا نهاية ($\infty$).

في عام 2006، كشف جوشوا بلوخ (Joshua Bloch) من Google عن خطأ برمجي ظل كامناً لمدة 9 سنوات في مكتبة Java القياسية (java.util.Arrays.binarySearch)، وهو خطأ الطفح الحسابي (Integer Overflow) في البحث الثنائي:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;
    while (low <= high) {
        int mid = (low + high) / 2; // ★ خطأ قاتل: طفح حسابي إلى عدد سالب عندما يكون low + high >= 2^31!
        int midVal = a[mid];
        if (midVal < key) low = mid + 1;
        else if (midVal > key) high = mid - 1;
        else return mid;
    }
    return -(low + 1);
}

عندما يتجاوز المجموع low + high الحد الأقصى لعدد صحيح بطول 32 بت ($2^{31} - 1 = 2,147,483,647$)، يتحول الناتج إلى عدد سالب، مما يؤدي فوراً إلى انهيار البرنامج بالاستثناء ArrayIndexOutOfBoundsException.

1.2 مسألة التوقف لتورينغ (1936) ومبرهنة رايس (1953)

لماذا لا نبتكر أداة تحليل ساكن تقرأ الكود المصدري لأي برنامج $P$ وتقرر بدقة 100% ما إذا كان خالياً من الأخطاء؟ تقف مسألة التوقف لآلان تورينغ (Halting Problem, 1936) ومبرهنة رايس (Rice’s Theorem, 1953) سداً منيعاً أمام ذلك:

أي أنه يستحيل رياضياً لأي أداة أن تجمع في وقت واحد بين: (1) الأتمتة الكاملة، و(2) السلامة المنطقية (Soundness: صفر نتائج سلبية كاذبة)، و(3) الاكتمال (Completeness: صفر إنذارات كاذبة).

1.3 كيف يتجاوز التحقق الصوري مبرهنة رايس؟ التقريب الأعلى السليم (Sound Over-Approximation)

يتمسك التحقق الصوري (Formal Verification) بشرط السلامة المنطقية (Soundness) دون أي مساومة: فإذا أعلنت الأداة أن البرنامج "SAFE"، فهو مضمون رياضياً بنسبة 100% ضد الأخطاء عبر جميع المسارات اللانهائية ($\infty$). ولتحقيق ذلك آلياً، تحسب الأداة تقريباً أعلى سليماً (Sound Over-Approximation) $\mathcal{R}_{\text{approx}} \supseteq \mathcal{R}_{\text{exact}}$ يحيط بجميع الحالات الممكنة، وتثبت أن تقاطعه مع حالات الخطأ $\mathcal{B}$ خالٍ تماماً:

  flowchart TD
    A["مجموعة الحالات الدقيقة R_exact للبرنامج P (غير قابلة للحسم وفق مبرهنة رايس)"] --> B["الأركان الأربعة للتحقق الصوري"]
    B --> C["الركن 1: التحقق الاستنتاجي (منطق فلويد-هور وSMT)"]
    B --> D["الركن 2: فحص النماذج Model Checking (المنطق الزمني وTLA+)"]
    B --> E["الركن 3: التفسير المجرد (روابط غالوا ومحلل Astrée)"]
    B --> F["الركن 4: إثبات النظريات التفاعلي (Coq / Lean 4 / Isabelle)"]
    C --> C1["لامتغيرات الحلقات I + إثبات آلي لشروط التحقق VC عبر Z3 SMT"]
    D --> D1["بنية كريبك M؛ استكشاف رمزي لـ 10^20 حالة عبر BDDs/SAT/IC3"]
    E --> E1["تقريب أعلى سليم آلي R_exact ⊆ γ(a#) يثبت أن γ(a#) ∩ Bad = ∅"]
    F --> F1["تشاكل كاري-هوارد: براهين رياضية تدققها نواة صغيرة موثوقة"]

2. الركن الأول: التحقق الاستنتاجي — منطق فلويد-هور، أضعف شرط مسبق، وحلّالات SMT

2.1 ثلاثية هور (Hoare Triple) ولامتغيرات الحلقات

في عام 1969، أسس توني هور (C. A. R. Hoare) منطق فلويد-هور القائم على ثلاثية هور:

• الصحة الجزئية (Partial Correctness): إذا تحقق الشرط المسبق $P$ قبل تنفيذ الأمر $C$، وإذا توقف $C$، فإن الشرط اللاحق $Q$ يتحقق حتماً بعده.
• الصحة الكلية (Total Correctness): تحت الشرط $P$، يتوقف $C$ حتماً في خطوات منتهية ويحقق $Q$.

تشمل قواعد الاستنتاج بديهية الإسناد $\{\,Q[E/x]\,\}\; x := E \;\{\,Q\,\}$، وقاعدة حلقة while المزودة بـ لامتغير الحلقة (Loop Invariant) $I$ ودالة الرتبة (Ranking Function) $V \in \mathbb{N}$ المتناقصة قطعيّاً:

وبفضل حساب أضعف شرط مسبق (Weakest Precondition, $\text{wp}(C, Q)$) الذي قدمه ديكسترا عام 1975، يتحول إثبات البرنامج إلى صيغ رياضية بحتة تُعرف بـ شروط التحقق (VCs): $P \implies \text{wp}(C, Q)$.

2.2 إثبات صحة البحث الثنائي باستخدام Dafny وحلّال Z3 SMT

عند تعديل حساب المنتصف إلى mid := low + (high - low) / 2 في لغة Dafny، يقوم حلّال Z3 SMT (المبني على معمارية DPLL(T) التي تدمج الدوال غير المفسرة EUF، والحساب الخطي الصحيح LIA، ومتجهات البتات $\mathcal{T}_{\text{BV}}$، ونظرية المصفوفات $\mathcal{T}_{\text{A}}$) بإثبات استحالة الطفح الحسابي وصحة الخوارزمية بنسبة 100% خلال أجزاء من الثانية:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= index ==> index < a.Length && a[index] == key
  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  var low := 0;
  var high := a.Length;
  while low < high
    invariant 0 <= low <= high <= a.Length
    invariant forall i :: 0 <= i < a.Length && !(low <= i < high) ==> a[i] != key
    decreases high - low
  {
    var mid := low + (high - low) / 2; // يثبت Z3 استحالة الطفح وأن 0 <= mid < a.Length!
    if a[mid] < key { low := mid + 1; }
    else if key < a[mid] { high := mid; }
    else { return mid; }
  }
  return -1;
}

3. الركن الثاني: فحص النماذج (Model Checking) والمنطق الزمني للأنظمة الموزعة

3.1 بنى كريبك والمنطق الزمني LTL / CTL

في عام 1981، ابتكر كلارك وإيمرسون وسيفاكيس (جائزة تورينغ 2007) تقنية فحص النماذج (Model Checking)، بينما طوّر ليزلي لامبورت (جائزة تورينغ 2013) لغة TLA+. يُنمذج النظام التزامني على هيئة بنية كريبك (Kripke Structure) $M = (S, S_0, R, L)$، وتُصاغ خصائصه بالمنطق الزمني الخطي LTL أو منطق شجرة الحساب CTL:

1. الأمان (Safety — «لا يحدث شيء سيئ أبداً»): الاستبعاد المتبادل: $$\text{LTL}: \quad \mathbf{G}\, \neg (\text{crit}_1 \land \text{crit}_2) \qquad \text{CTL}: \quad \mathbf{AG}\, \neg (\text{crit}_1 \land \text{crit}_2)$$
2. الحيوية (Liveness — «الشيء الجيد سيحدث حتماً في النهاية»): عدم المجاعة (Starvation Freedom): $$\text{LTL}: \quad \mathbf{G}\, (\text{req}_1 \implies \mathbf{F}\, \text{crit}_1) \qquad \text{CTL}: \quad \mathbf{AG}\, (\text{req}_1 \implies \mathbf{AF}\, \text{crit}_1)$$

3.2 آلات بوخي، ومخططات القرار الثنائي BDD، وقصة نجاح TLA+ في AWS

يحوّل فاحص النماذج نفي الخاصية $\neg \varphi$ إلى آلة بوخي (Büchi Automaton) $A_{\neg \varphi}$، ثم يفحص فراغ الجداء المتزامن ($\mathcal{L}(M \times A_{\neg \varphi}) = \emptyset$). وللتغلب على انفجار فضاء الحالات، تُستخدم مخططات القرار الثنائي (BDDs، براينت 1986 / ماكميلان 1990) القادرة على فحص $10^{20}$ حالة، إضافة إلى الفحص المحدود (BMC) وخوارزمية IC3 / PDR.

في Amazon Web Services (AWS)، مكّن استخدام TLA+ (TLC) في تصميم S3 وDynamoDB من اكتشاف خطأ خفي يؤدي لفقدان البيانات ويتطلب تسلسلاً دقيقاً من 35 خطوة متداخلة من انقطاعات الشبكة وتأخر الرسائل، وذلك قبل كتابة سطر واحد من الكود الإنتاجي!

4. الركن الثالث: التفسير المجرد ودرس كارثة صاروخ أريان 5

4.1 4 يونيو 1996: لماذا انفجر صاروخ أريان 5 البالغة تكلفته 370 مليون دولار بعد 37 ثانية؟

في 4 يونيو 1996، انفجر صاروخ Ariane 5 الأوروبي في رحلته الأولى (Flight 501) بعد 37 ثانية فقط من إطلاقه، مسبباً خسائر بقيمة 370 مليون دولار. كان السبب إعادة استخدام وحدة برمجية بلغة Ada من صاروخ Ariane 4 داخل نظام الملاحة بالقصور الذاتي (SRI)، حيث كانت تحوّل متغيراً عشرياً بطول 64 بت يمثل السرعة الأفقية (BH) إلى عدد صحيح بطول 16 بت ($-32,768 \dots +32,767$). وبسبب التسارع الهائل لصاروخ Ariane 5، تجاوزت قيمة BH سقف $32,767$، مما أطلق استثناء طفح حسابي عتادي (Operand Error) غير معالج. توقف الحاسوب الاحتياطي والرئيسي، وأرسلا نمط بتات تشخيصي إلى حاسوب التوجيه الرئيسي (OBC) الذي ظنه بيانات انحراف حقيقية، فوجه فوهات الدفع إلى أقصى زاوية مما أدى لتفكك الصاروخ في الجو.

4.2 التفسير المجرد لكوزو (1977)، وروابط غالوا، وإنجاز Astrée في طائرة Airbus A380

يربط التفسير المجرد (Abstract Interpretation) الذي ابتكره باتريك كوزو وراضية كوزو عام 1977 بين الشبكة الملموسة $(\mathcal{C}, \subseteq) = (\mathcal{P}(\Sigma), \subseteq)$ والمجال المجرد $(\mathcal{A}, \sqsubseteq^\#)$ (كالفترات $[a,b]$، والمثمنات $\pm x \pm y \le c$، ومتعددات الوجوه المحدبة) عبر رابطة غالوا (Galois Connection):

ومع شرط السلامة المحلية $\alpha(F(\gamma(a^\#))) \sqsubseteq^\# F^\#(a^\#)$ ومؤثر التوسيع (Widening $\nabla$)، تحيط النقطة الثابتة المجردة بجميع الحالات الممكنة بنسبة أمان 100%:

  flowchart TD
    subgraph Concrete["المجال الملموس C = P(Σ) (لانهائي / غير قابل للحسم)"]
        S["مجموعة الحالات الملموسة S"] -->|"الانتقال الملموس F"| FS["الحالات التالية F(S)"]
        LFP_C["الحالات الممكنة الدقيقة R_exact = lfp F"]
    end
    subgraph Abstract["المجال المجرد A (الفترات / المثمنات / المجسمات الإهليلجية)"]
        A_elem["الحالة المجردة a#"] -->|"الانتقال المجرد F#"| FA["الحالة المجردة التالية F#(a#)"]
        LFP_A["النقطة الثابتة المجردة lfp F# (تقارب سريع عبر Widening ∇)"]
    end
    S -->|"التجريد α(S)"| A_elem
    FA -->|"التجسيد γ(F#(a#)) ⊇ F(S)"| FS
    LFP_A -->|"ضمان رياضي تام: R_exact ⊆ γ(lfp F#)"| LFP_C

نجح المحلل الساكن Astrée في التحقق آلياً من برمجيات التحكم بالطيران Fly-by-Wire لطائرة Airbus A380 (نحو مليون سطر من كود C) مع صفر إنذارات كاذبة، مثبتاً رياضياً استحالة حدوث أي خطأ تشغيلي!

5. الركن الرابع: مبرهنات النظريات التفاعلية (Coq / Lean 4 / Isabelle) والمقارنة الشاملة

استناداً إلى تشاكل كاري-هوارد (Curry-Howard Isomorphism) (القضايا المنطقية هي أنواع، والبراهين هي برامج)، حققت الأنظمة التفاعلية (Coq / Rocq وLean 4 وIsabelle/HOL) معجزتين صناعيتين:

1. CompCert (Xavier Leroy, INRIA): مصرّف C محسّن موثق بالكامل في Coq. في اختبار Csmith الشهير (PLDI 2011)، وُجد أكثر من 325 خطأ ترجمة في GCC وLLVM، بينما سجل الجزء الموثق من CompCert صفر أخطاء!
2. seL4 (Gerwin Klein et al.): أول نواة نظام تشغيل مصغرة في العالم يتم إثبات صحتها الوظيفية وأمنها بالكامل في Isabelle/HOL حتى مستوى الكود الثنائي لمعالجات ARM وRISC-V.