مدخل إلى التحقّق الشكلي باستخدام SPARK ── من عقود Ada إلى البرهان الرياضي

1. مقدّمة ── ما وراء «التشغيل والتحقّق»

أكثر الطرق شيوعاً لضمان جودة البرمجيّات هو الاختبار (testing).

الاختبار: يتحقّق من أنّ البرنامج يعمل بشكل صحيح للمدخلات المُختارة

لكنّ الاختبار له حدود جوهريّة. عدد المدخلات الممكنة غير محدود، ولا يمكن للاختبار وحده إثبات الصحّة لكلّ المدخلات.

هنا يأتي دور التحقق الشكلي (Formal Verification).

التحقق الشكلي: يُثبت رياضيّاً أنّ خاصيّة ما تتحقّق لكلّ المدخلات الممكنة

المقال السابق «جاذبيّة لغة Ada» قدّم نظرة عامّة على Ada، وتطرّق إلى SPARK بإيجاز.

يركّز هذا المقال تحديداً على التطبيق العمليّ للتحقّق الشكلي باستخدام SPARK، ويتناول ما يلي:

ما هو SPARK وعلاقته بـ Ada
كيفيّة كتابة العقود (Pre/Post)
كيفيّة إثباتها باستخدام GNATprove
كيفيّة تصميم ثوابت الحلقات
كيفيّة إدارة الآثار الجانبيّة عبر عقود تدفّق البيانات (Global/Depends)
استراتيجيّة تبنٍّ تدريجيّة عبر مستويات البرهان (من Stone إلى Platinum)
كيفيّة دمج SPARK في مشاريع حقيقيّة

الهدف هو أن تعيش تجربة الانتقال من الاختبار إلى البرهان من خلال أمثلة شيفرة عمليّة.

قرّاء هذا المقال والمعرفة المسبقة

القرّاء المتوقَّعون هم كالتالي.

• من اطّلع مرّة على النحو الأساسيّ لـ Ada (الحزم، وأنماط المعاملات in / out / in out، والأنواع والأنواع الفرعيّة)
• من يهتمّ بالبرمجة بالعقود أو التحليل الساكن ويبحث عن «ما بعد الاختبار»
• من يدرس وسائل ضمان الجودة في برمجيّات عالية الموثوقيّة أو مدمجة أو تحكّميّة

يمكن القراءة دون خبرة Ada، لكن نكمّل مقدّمتين فقط. تتكرّر في أمثلة هذا المقال فصل مواصفة الحزمة عن جسمها عبر package ... is وpackage body ... is، وأنماط المعاملات مثل procedure P (X : in out Integer). إن لم تكن هاتان مألوفتين، ابدأ بأساسيّات Ada في «جاذبيّة لغة Ada» ثمّ عُد؛ عندها يمكن التركيز على العقود.

وبالعكس، يكفي فهم هاتين للمتابعة. ترميز SPARK الخاصّ (SPARK_Mode وPre وPost وLoop_Invariant وGlobal وDepends) يُشرح كلّه داخل هذا المقال. لا حاجة لنظريّة المُثبِتات أو للمنطق الرياضيّ. تقرأ رسالة GNATprove ثمّ تصلّح الشيفرة أو العقد. هذا ما يلزم فعلاً.

مقتطفات الشيفرة الواردة في هذا المقال متاحة، مرتَّبة حسب الفصول، كمجموعة مرجعيّة على GitHub.

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

في المخطّط، يشير الخطّ المتّصل إلى علاقة قائمة دائماً، ويشير الخطّ المتقطّع إلى علاقة مشروطة (شروط قيامها مذكورة في شرح كلّ علاقة في الصفحة التفصيليّة). القائمة الكاملة للعلاقات (المجموع 17، مع الأدلّة ودرجة اليقين) وتعريفات المفاهيم الرئيسة مجمّعة في صفحة تفاصيل خريطة المعرفة (باليابانية). البيانات: JSON-LD / Turtle

2. ما هو SPARK ── المجموعة الفرعيّة من Ada وبوّابة الدخول إلى عالم البرهان

SPARK هو مجموعة فرعيّة (subset) من لغة Ada.

كونه مجموعة فرعيّة قرار تصميميّ مقصود.

Ada الكاملة → تعبيريّة عالية، لكنّ التحقّق منها بالكامل غير واقعيّ
SPARK       → مقتصر على الميزات القابلة للتحقّق، ما يجعل البرهان واقعيّاً

أهمّ ما يقيّده SPARK هو:

إدارة الذاكرة الديناميكيّة عبر المؤشّرات (access types) → مضبوطة بنموذج ملكيّة (ownership)
الاستخدام الحرّ لمعالِجات الاستثناءات               → مسموح به بشكل مقيَّد
بِنى البيانات المتكرّرة (recursive)                   → مقيَّدة لصعوبة إثباتها
الاستخدام الحرّ للمهامّ (tasking)                     → مقيَّد عبر ملف Ravenscar

قد تبدو كلمة «قيود» ضيّقة، لكنّ هذه القيود هي ثمن قابليّة الإثبات.

محور مجموعة أدوات SPARK هو GNATprove المقدَّمة من AdaCore.

آليّة عمل GNATprove:
1. تحليل شيفرة Ada الموسومة بـ SPARK
2. ترجمة العقود (Pre/Post) والتوكيدات (assertions) إلى اللغة الوسيطة Why3
3. محاولة الإثبات باستخدام مُثبِتات آليّة مثل Z3 وcvc5 وAlt-Ergo
4. الإبلاغ عن النتائج كرسائل مباشرة على الشيفرة المصدريّة

الشكل التالي يلخّص هذا التدفّق.

flowchart LR
    Src["شيفرة Ada مكتوبة بـ SPARK<br/>Pre / Post / Assert"] --> GP[GNATprove]
    GP --> VC[توليد شروط التحقّق]
    VC --> Why3["Why3<br/>لغة وسيطة ومنصّة برهان"]
    Why3 --> P1[cvc5]
    Why3 --> P2[Z3]
    Why3 --> P3[Alt-Ergo]
    P1 --> Res[تجميع النتائج]
    P2 --> Res
    P3 --> Res
    Res --> Msg["رسائل بموقع في الشيفرة المصدريّة<br/>info / medium / high"]

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

الأسماء التي ظهرت في هذا الفصل

نثبّت هنا الأسماء العلم عند أوّل ظهور. بعد ذلك نستخدمها دون شرح.

النقطة الجوهريّة: SPARK مبنيّ فوق Ada.

شيفرة SPARK = شيفرة Ada + توضيحات العقود

بعبارة أخرى، SPARK امتداد طبيعيّ لتطوير Ada المعتاد. لا حاجة لتعلّم صياغة جديدة كلّيّاً.

3. تثبيت GNATprove وأوّل برهان

لنبدأ بإعداد بيئة لتشغيل GNATprove.

تثبيت Alire

GNATprove مرفق مع سلسلة أدوات GNAT. أسهل طريقة للحصول على هذه السلسلة هي Alire. هو مدير حزم مصدريّ لـ Ada / SPARK، واسم الأمر alr. تُحمَّل التوزيعات من صفحة الإصدارات في مستودع Alire على GitHub.

بعد التثبيت اختر المترجم الافتراضيّ.

alr toolchain --select

يفتح مساعد الاختيار قائمة بمركّبات GNAT المتاحة لتختار المترجم الافتراضيّ. تشغيل alr toolchain بلا وسائط يعرض المترجمات المثبَّتة والافتراضيّ الحاليّ.

التحقّق من الإصدار

بعد جاهزيّة البيئة سجّل الإصدارات. نتائج البرهان تعتمد على إصدار المُثبِت. هذه أوّل معلومة تُراجَع لاحقاً عندما «لم يعد بالإمكان إثبات الشيفرة نفسها».

alr version
gnatprove --version

إنشاء المشروع

باستخدام Alire، يمكن إنشاء مشروع جاهز لـ SPARK بالأمر التالي:

alr init --bin spark_demo
cd spark_demo

بما أنّ GNATprove مرفق مع مترجم GNAT، فإنّ الأمر gnatprove متاح فور نجاح بناء المشروع بـ alr build.

كأوّل هدف للبرهان، لنكتب دالّة تُعيد القيمة المطلقة.

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

أبرز النقاط الجديرة بالملاحظة:

تُضاف with SPARK_Mode إلى مواصفة الحزمة (package spec) وجسمها (body) معاً
شرط Post يعلن الخاصيّة «النتيجة غير سالبة»
السمة 'Result تشير إلى قيمة الدالّة المُعادة

الآن لنشغّل GNATprove على هذه الشيفرة:

gnatprove -P spark_demo.gpr

تكون النتيجة كالتالي:

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

رسالة postcondition proved تعني أنّه تمّ إثبات رياضيّاً أنّ القيمة المُعادة غير سالبة لكلّ قيم Integer الممكنة.

هذه هي تجربة الدخول إلى عالم SPARK.

الخرج عندما يتعذّر الإثبات

النظر إلى خرج النجاح وحده لا يكفي في العمل؛ ما يلزم هو قراءة الفشل. يبلّغ GNATprove عن الفحوصات التي لم تُثبَت بموقع في الشيفرة المصدريّة. الشكل الأساسيّ سطر واحد كالتالي.

file.adb:12:37: medium: divide by zero might fail

المعنى: في file.adb السطر 12 العمود 37، أي عند علامة القسمة /، «لم يُثبَت أنّ المقسوم عليه ليس صفراً». المهمّ أنّها might fail (قد تفشل) وليست will fail (ستفشل). ليس بالضرورة أن يكون هناك خطأ حقيقيّ. في أغلب الحالات المعلومات ناقصة فلم يستطع المُثبِت الحكم.

عند الحصول على مثال مضادّ يكون التقرير أوضح.

high: assertion might fail
--> counterex.adb:11:25
 11 |    pragma Assert (R < 42);
    |                  ^~~~~~
  + e.g. when R = 42
  + provers gave up before completing the proof

e.g. when R = 42 مثال مضادّ يقول صراحة «لا تتحقّق عندما يكون R = 42». إذا خمّن GNATprove أنّ السبب نقص في العقد، قد يُرفق اقتراح إصلاح.

possible fix: subprogram at line xxx should mention Var in a precondition
possible fix: loop at line xxx should mention Var in a loop invariant
possible fix: call at line xxx should mention Var in a postcondition

أسرع طريق للاعتياد على هذه الرسائل هو إخراجها عمداً. مثلاً غيّر Post في Abs_Value أعلاه إلى Abs_Value'Result > 0 (أكبر من صفر) فيتعذّر إثبات حالة X = 0 وتظهر postcondition might fail. إن نزعت Pre من Increment في الفصل 5 تظهر overflow check might fail. التناوب بين أمثلة النجاح والفشل أقصر طريق للاعتياد على GNATprove.

مستويات الخطورة (info / medium / high) وأنواع الفحص مرتَّبة في الفصل 12.

4. أساسيّات التصميم بالعقد ── كتابة Pre وPost

تبدأ إثباتات SPARK بكتابة العقود.

العقود ميزة لغويّة في Ada 2012، لكنّها في SPARK تصبح مُدخَل البرهان.

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

إليك مبادئ تصميم Pre وPost:

Pre (الشرط المسبق):
  مسؤوليّة الطرف المستدعي (caller)
  «إن استدعيتني مستوفياً هذا الشرط، أضمن لك Post»
  ضعيف بما يكفي ليكون قابلاً للتحقيق، وقويّ بما يكفي ليكون مفيداً

Post (الشرط اللاحق):
  مسؤوليّة التنفيذ
  «بعد الاستدعاء، يكون العالَم في هذه الحالة»
  السمة 'Old تشير إلى القيم قبل الاستدعاء
  إن كان قويّاً جدّاً ضيَّق التنفيذ؛ وإن كان ضعيفاً جدّاً لم يُثبت شيئاً مفيداً

أخطاء شائعة وطرق تجنّبها:

الخطأ 1: Pre قويّ جدّاً
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → تحقّق: هل يستطيع الطرف المستدعي دائماً استيفاء هذا الشرط؟
  → لا تُضيّق Pre لمجرّد أنّ الاختبارات تنجح

الخطأ 2: Post ضعيف جدّاً
  Post => True
  → لا يضمن شيئاً. البرهان بلا معنى.

الخطأ 3: نسيان الآثار الجانبيّة في Post
  Post => Result = X * 2  (إغفال تحديث متغيّر عامّ)
  → اجعل الآثار الجانبيّة صريحة عبر عقود Global/Depends (القسم 9)

5. إثبات خلوّ الحساب من تجاوز السعة ── ضمان الأمان العدديّ

من أكثر ما يُثبته SPARK قيمةً في الممارسة العمليّة هو خلوّ الحساب من تجاوز السعة (overflow).

انظر إلى هذه الشيفرة:

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

Pre => X < Integer'Last هو المفتاح. بوجود هذا العقد، يستطيع GNATprove إثبات أنّ الجمع لن يتجاوز السعة.

في غياب العقد، يُحذِّر GNATprove من احتمال تجاوز السعة:

medium: overflow check might fail

الأمر نفسه ينطبق على حسابات أكثر تعقيداً:

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

يبدو الشرط Pre معقّداً، لكنّه ببساطة يعبّر عن أنّ «مجموع A وB لا يتجاوز السعة»، مقسَّماً حسب الحالات وفقاً للإشارة.

الفكرة الجوهريّة:
  جوهر إثبات خلوّ الحساب من تجاوز السعة هو الإعلان في Pre أنّ نتيجة
  الجمع أو الضرب تقع ضمن مدى النوع
  قد يبدو الأمر مُتعِباً، لكن بمجرّد كتابته لن يزعجك خطأ تجاوز السعة
  ثانيةً أبداً

6. ثوابت الحلقات ── إثبات خصائص الحلقات

من أصعب أجزاء التحقق الشكلي إثبات خصائص الحلقات.

تُنفَّذ الحلقات عدداً غير محدَّد من المرّات، فلا يستطيع الاختبار تغطية كلّ الحالات. يستخدم SPARK لذلك ثوابت الحلقات (Loop Invariants).

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

يتطلّب تصميم ثوابت الحلقات طريقة التفكير التالية:

1. اكتب خاصيّة تتحقّق في بداية كلّ تكرار
2. اختر خاصيّة تستلزم، بعد آخر تكرار، الشرط اللاحق Post المطلوب
3. يعبّر الثابت عن الحساب الجزئيّ حتّى تلك النقطة في صورة صيغة رياضيّة

إليك مثالاً آخر: البحث في مصفوفة (array).

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

الثابت هنا هو: «في النطاق المفحوص حتّى الآن، لا يوجد Target».

مبادئ تصميم ثوابت الحلقات:
  عبِّر بصيغة رياضيّة: «ماذا يمكن أن نقوله بعد n تكراراً؟»
  في حلقات المصفوفات، النمط الشائع هو «بالنسبة للنطاق المُعالَج حتّى الآن، تتحقّق P»
  الثابت القويّ جدّاً يتعذّر إثباته؛ والضعيف جدّاً لا يستلزم Post
  إيجاد التوازن الصحيح هو جوهر مهارة إثبات الحلقات

7. توكيدات pragma Assert ── خصائص جزئيّة داخل الشيفرة

بالإضافة إلى العقود (Pre/Post)، يسمح SPARK بكتابة توكيدات (Assert) مباشرة داخل جسم الشيفرة.

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

استخدامات pragma المختلفة:

Pre/Post:       وعود عند دخول الإجراء الفرعيّ (subprogram) والخروج منه
Assert:         خاصيّة يجب أن تتحقّق عند نقطة محدَّدة في الشيفرة
Loop_Invariant: خاصيّة تُحفَظ في كلّ تكرار من الحلقة
Loop_Variant:   كمّيّة متناقصة تُستخدم لإثبات انتهاء الحلقة

حالات استخدام جيّدة لـ Assert:

التحقّق من نتائج وسيطة لحسابات معقّدة
التحقّق من الحالة بعد تفرّع if/else
تأكيد خصائص القيم المُعادة بعد استدعاء إجراء
توفير مُسلّمات (lemmas) تُسهِّل الإثباتات اللاحقة

8. عقود تدفّق البيانات ── Global وDepends

من الميزات القويّة في SPARK عقود تدفّق البيانات.

تعلن هذه العقود صراحةً عن المتغيّرات العامّة (global variables) التي يقرأها الإجراء الفرعيّ ويكتب إليها.

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

أنماط عقد Global هي:

Input:  قراءة فقط (للدوال)
Output: كتابة فقط (للتهيئة)
In_Out: قراءة وكتابة (للتحديثات)

علاوة على ذلك، يمكن التعبير عن الاعتماديّات بين المتغيّرات بـ Depends:

procedure Transfer
  (From, To : in out Account)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+ تعني «يعتمد على القيمة السابقة بالإضافة إلى هذه المدخلات الإضافيّة».

فوائد عقود تدفّق البيانات:
  1. «بماذا تتّصل هذه الدالّة؟» يظهر بنظرة واحدة
  2. تُكتشف الآثار الجانبيّة غير المقصودة وقت الترجمة (compile time)
  3. تُغذّي تحليل تدفّق المعلومات للمتغيّرات
  4. تساعد على تصوّر تدفّق البيانات في الأنظمة الكبيرة

9. مستويات البرهان ── تبنٍّ تدريجيّ من Stone إلى Platinum

لدى SPARK مفهوم مستوى البرهان (Proof Level).

محاولة إثبات كلّ الشيفرة إثباتاً كاملاً دفعة واحدة كثيراً ما تؤدّي إلى الإحباط. لذا يقدّم SPARK استراتيجيّة لرفع صرامة البرهان تدريجيّاً.

Stone:
  التحقّق من أنّ الشيفرة SPARK صالحة كمجموعة فرعيّة
  يُستخدَم كمرحلة وسطى أثناء الإدخال

Bronze:
  Stone + عدم قراءة متغيّرات غير مُهيَّأة،
  وضمان أنّ تدفّق البيانات كما هو مقصود
  يُطبَّق على أوسع نطاق ممكن

Silver:
  Bronze + إثبات عدم وقوع أخطاء وقت التشغيل
  (خارج النطاق، وتجاوز السعة، والقسمة على صفر)
  (AoRTE: Absence of Run-time Errors)
  الهدف الافتراضيّ للبرمجيّات الحرجة

Gold:
  Silver + خصائص نزاهة (integrity) مهمّة
  (خصائص مفتاحيّة للسلامة والأمان)
  يُطبَّق فقط على جزء الشيفرة الذي يحمل تلك الخصائص

Platinum:
  إثبات الصحّة الوظيفيّة الكاملة لمتطلّبات المواصفة
  يُطبَّق فقط حيث توجد أعلى المتطلّبات
  التكلفة مرتفعة وأمثلة التطبيق قليلة

ما الذي تعنيه كلمة «مستوى» ── --mode و--level ليسا الشيء نفسه

نرتّب هنا نقطة يسهل الخلط بينها. Stone إلى Platinum هي مستويات ضمان البرمجيّات، وهي مفهوم مختلف عن خيار --level في gnatprove. ما يقابلها هو --mode.

Silver وGold وPlatinum تُشغَّل بالمفتاح نفسه. الفرق ليس في طريقة تشغيل الأداة، بل في ما تحدّده هدفاً للتحقّق وإلى أيّ مدى.

أمّا --level=0 إلى --level=4 فإعدادات مسبقة تحدّد كم من الجهد يُبذَل في البرهان. رفع القيمة يزيد الوقت ويزيد قدرة الإثبات. المحتوى تركيب من مفاتيح منفردة كالتالي.

أي أنّ --mode هو «ماذا نتحقّق منه»، و--level هو «كم نُصرّ». ما ينبغي الانتباه إليه أوّلاً هو --mode؛ أمّا --level فمقبض ضبط يُرفع عندما يتعذّر الإثبات.

تنبيه عمليّ آخر: لأنّ --level يُضبَط بحدّ زمنيّ، تتغيّر النتيجة حسب أداء الآلة والحمل، ولا تكرار لها. في CI أو عند مشاركة النتائج بين عدّة أشخاص، توصي الوثائق الرسميّة باستخدام --steps الذي يحدّ السقف بعدد خطوات الاستدلال لا بالوقت، أو --replay الذي يعيد نتائج برهان قائمة.

المصدر: SPARK User’s Guide (8.1 Levels of Software Assurance، وAppendix A Command Line Invocation)

استراتيجيّة إدخال عمليّة كالتالي.

المرحلة 1: إيصال المشروع بأكمله إلى مستوى Stone
  → اكتشاف أخطاء كتابة العقود

المرحلة 2: جعل الوحدات المهمّة عند مستوى Silver
  → القضاء على تجاوز السعة والوصول خارج النطاق
  → كثير من أخطاء العمل الفعليّ تُمنَع هنا

المرحلة 3: جعل المنطق الجوهريّ عند مستوى Gold
  → ضمان رياضيّ لخصائص مفتاحيّة للسلامة والأمان
  → لا الشيفرة كلّها، بل الجزء الذي يحمل تلك الخصائص

المرحلة 4: Platinum فقط حيث توجد أعلى المتطلّبات
  → إثبات الصحّة الوظيفيّة الكاملة لمتطلّبات المواصفة
  → النطاق أدنى ما يمكن لأنّ التكلفة مرتفعة

10. سير عمل عمليّ للبرهان ── تقليل إعادة العمل

إليك سير عمل لاستخدام GNATprove في العمل اليوميّ:

1. صمِّم الأنواع والمواصفات
   حدِّد قيود المدى وثوابت الأنواع

2. اكتب العقود (Pre/Post)
   عبِّر عن المواصفة كعقود قبل التنفيذ

3. اجعل الشيفرة تُترجَم بنجاح
   أصلح أخطاء الترجمة باستخدام GNAT

4. شغِّل GNATprove عند مستوى Stone
   gnatprove -P proj.gpr --mode=stone

5. راجع التحذيرات ونقِّح العقود عند الحاجة
   انتبه بشكل خاصّ لتسريب التهيئة
   لرؤية التهيئة وتدفّق البيانات فقط استخدم Bronze
   gnatprove -P proj.gpr --mode=bronze

6. استهدف مستوى Silver
   gnatprove -P proj.gpr --mode=silver
   اقضِ على أخطاء وقت التشغيل

7. أضف ثوابت للحلقات إن وُجدت
   إن تعذّر الإثبات، تحقّق ممّا إذا كانت الثوابت ناقصة

8. أثبت خصائص مهمّة عند مستوى Gold
   gnatprove -P proj.gpr --mode=gold
   مفتاح التشغيل نفسه لـ Silver؛ ما يتغيّر هو هدف التحقّق
   ارفع --level فقط عندما لا ينتهي الإثبات في الوقت
   مثال: gnatprove -P proj.gpr --mode=gold --level=3

حالات شائعة من نوع «تعذّر الإثبات» وطرق التعامل معها:

الحالة 1: «medium: postcondition might fail»
  → Post قويّ جدّاً، أو Pre ضعيف جدّاً
  → أو ثوابت الحلقة غير كافية

الحالة 2: «medium: overflow check might fail»
  → قيِّد مدى القيم في Pre
  → أو ضيِّق مدى النوع نفسه

الحالة 3: «medium: array index check might fail»
  → استخدم ثابت حلقة لإثبات أنّ مدى الحلقة يقع ضمن حدود المصفوفة
  → استخدم for I in Arr'Range لمساعدة SPARK على التعرّف التلقائيّ
    على الحدود

الحالة 4: «prover timeout»
  → انتهى الوقت المتاح للمُثبِت؛ قسِّم البرهان بثوابت تدريجيّة
  → قسِّم الدوال الكبيرة إلى دوال أصغر

11. الجمع بين SPARK والاختبار ── فهم العلاقة التكامليّة

التحقق الشكلي والاختبار ليسا خصمَين، بل يكمِّلان بعضهما.

إثباتات SPARK:
  تُثبت الخصائص لكلّ المدخلات الممكنة
  تغطّي فقط الخصائص المكتوبة في العقود
  الحالات التي يتعذّر إثباتها تُترَك للمراجعة اليدويّة أو الاختبار

الاختبار:
  يتحقّق من السلوك الفعليّ للمدخلات المُختارة
  يمكنه اكتشاف افتراضات ضمنيّة غير مكتوبة في العقود
  يمكنه التحقّق من التفاعل مع بيئة التشغيل

أنماط الاستخدام المشترك:

1. ضمان خلوّ البرنامج من أخطاء التشغيل (مستوى Silver) باستخدام SPARK
2. التحقّق من صحّة مدخلات ومخرجات محدَّدة باختبارات الوحدة
3. إثبات المنطق الأساسيّ عند مستوى Gold
4. تركيز الاختبار على الأجزاء التي يتعذّر إثباتها

تملك Ada إطار عمل لاختبارات الوحدة يُدعى AUnit. المزيج العمليّ هو تثبيت الأنواع والعقود بـ SPARK، ثمّ اختبار السلوك بـ AUnit.

12. قراءة نتائج GNATprove ── تفسير الرسائل

مخرجات GNATprove لها ثلاثة مستويات من الخطورة:

info:   نجح البرهان
medium: فشل البرهان (تحذير). يلزم مراجعة يدويّة
high:   فشل البرهان (خطأ). احتمال كبير لانتهاك العقد

رسائل شائعة ومعناها:

«postcondition proved»          تمّ إثبات شرط Post
«range check proved»            تمّ إثبات فحص المدى
«overflow check proved»         تمّ إثبات خلوّ الحساب من تجاوز السعة
«index check proved»            تمّ إثبات حدود فهرس المصفوفة
«divide by zero check proved»   تمّ إثبات خلوّ الحساب من القسمة على صفر

«might fail»                    تعذّر الإثبات
«cannot prove»                  لم يستطع المُثبِت إتمام البرهان
«prover timeout»                لم يكتمل البرهان ضمن الوقت المحدَّد

خطوات التعامل مع might fail:

1. اقرأ الشيفرة واحكم هل يمكن أن تفشل فعلاً
2. إن كانت قابلة للفشل، أصلح الشيفرة
3. إن كان يُفترَض ألّا تفشل، قوِّ العقد (Pre / الثابت)
4. إن ظلّ الإثبات متعذّراً، أعلنها افتراضاً عبر pragma Assume
   (تنبيه: Assume افتراض غير مُثبَت، فاستخدمه بحذر)

13. كيفيّة الدمج في مشاريع حقيقيّة

نهج واقعيّ لإدخال SPARK إلى مشروع قائم:

1. ابدأ بالشيفرة الجديدة
   لا تحاول تحويل كلّ الشيفرة القائمة إلى SPARK دفعة واحدة
   فعِّل SPARK_Mode في الوحدات المكتوبة حديثاً

2. استهدف Silver
   Gold (إثبات نزاهة مهمّة) وPlatinum (برهان وظيفيّ كامل) مثاليّان،
   لكن ابدأ بـ Silver (غياب أخطاء وقت التشغيل)
   حتّى مجرّد منع تجاوز السعة له قيمة عمليّة كبيرة

3. اكتب العقود بدءاً من الواجهات
   اكتب العقود في مواصفة الحزمة (.ads) قبل التنفيذ
   بوجود مواصفة راسخة، يستطيع أيّ مُنفِّذ كتابة شيفرة تستوفي العقود

4. ادمج في CI/CD
   أضف gnatprove إلى خطّ أنابيب CI (CI pipeline)
   أوقف البناء (أو على الأقلّ حذِّر) عند فشل الإثبات

5. اجمع تقارير البرهان
   ولِّد التقارير بـ gnatprove --report=all
   تتبَّع تطوّر العناصر غير المُثبَتة عبر الزمن

للمشاريع التي تخلط شيفرة C/C++ مع Ada، يفيد نهج تدريجيّ:

1. اكتب الوحدات الجديدة بلغة Ada/SPARK
2. تواصل مع C/C++ عبر Interfaces.C
3. انقل بِنى البيانات الحرِجة ومنطق التحقّق إلى SPARK
4. وسِّع نطاق SPARK تدريجيّاً

14. حدود SPARK ونقاط يجب الانتباه إليها

SPARK ليس حلّاً سحريّاً أيضاً. فهم حدوده بصدق يقود إلى تطبيقه بشكل صحيح.

ما يستطيع SPARK إثباته:
  يُثبت SPARK فقط الخصائص المكتوبة في العقود
  الخصائص المُغفَلة (التي نسيت كتابتها) لا تُثبَت
  مثال: إثبات أنّ النتيجة مُرتَّبة في Post لا يضمن الحفاظ على العناصر
  الأصليّة ما لم تُكتَب هذه الخاصيّة أيضاً

حدود المُثبِتات:
  بعض الخصائص المعقّدة تتجاوز قدرات المُثبِتات الآليّة
  في هذه الحالات يلزم البرهان التفاعليّ (مثل Coq)
  ومع ذلك، يكفي البرهان الآليّ في مُعظَم الحالات العمليّة

قيود اللغة:
  الشيفرة المُكثِّفة استخدام المؤشّرات لا يمكن تحويلها إلى SPARK
  إثبات التخصيص الديناميكيّ للذاكرة محدود
  إثبات بِنى البيانات المتكرّرة صعب

إتقان المطوّرين:
  كتابة العقود تتطلّب تدريباً
  تصميم ثوابت الحلقات يستغرق وقتاً طويلاً بشكل خاصّ لإتقانه
  خطّة رفع مهارات الفريق بأكمله ضروريّة لا غنى عنها

15. الخلاصة ── جعل البرهان جزءاً من التطوير اليوميّ

استعرضنا ممارسة التحقق الشكلي باستخدام SPARK.

SPARK مجموعة فرعيّة من Ada، مقتصرة على الميزات القابلة للتحقّق
العقود (Pre/Post) هي مُدخَل الإثباتات. عقود Ada 2012 تعمل مباشرة
GNATprove يُنفِّذ إثباتات آليّة ويُبلِغ عن النتائج على مستوى الشيفرة
المصدريّة
ثوابت الحلقات تُثبت خصائص الحلقات
Global/Depends يجعلان تدفّق البيانات صريحاً ويديران الآثار الجانبيّة
مستويات البرهان (من Stone إلى Platinum) تتيح زيادة الصرامة تدريجيّاً
استهداف مستوى Silver أوّلاً (خلوّ من أخطاء التشغيل) هو التوصية العمليّة
الاختبار والبرهان ليسا متضادَّين ── بل يكمِّلان بعضهما

قد يكون لديك انطباع مسبَق بأنّ «التحقق الشكلي صعب جدّاً ومقتصر على مشاريع خاصّة».

لكنّ مزيج SPARK وGNATprove اليوم بلغ المستوى التالي:

1. اكتب عقداً. هذا في جوهره نشاط تصميميّ مماثل لكتابة الأنواع أو الاختبارات
2. شغِّل gnatprove. يشعر الأمر وكأنّه ترجمة (compilation)
3. انظر إلى النتائج وأصلح الشيفرة أو العقد

هذه الدورة لا تختلف عن سير التطوير اليوميّ المعتاد الذي تُصلِح فيه الشيفرة بالاستناد إلى رسائل خطأ المترجم (compiler).

الفرق هو التالي: بينما يضمن المترجم أنّ «الصياغة صحيحة»، يضمن GNATprove «الصحّة لكلّ المدخلات».

شعار Ada الذي قُدِّم في المقال السابق ── «الأخطاء لا تُكتشَف، بل تجعلها الأنواع والعقود مستحيلة الكتابة أصلاً» ── يتقدّم مع SPARK إلى المستوى التالي:

غياب الأخطاء تضمنه البراهين.

ابدأ بإضافة SPARK_Mode وشرط Post إلى دالّة صغيرة، ثمّ شغِّل gnatprove.

عندما ترى الرسالة الخضراء postcondition proved، ستتغيّر نظرتك إلى ضمان جودة البرمجيّات.

روابط مرجعية

• مجموعة شيفرة مرجعيّة مرتَّبة حسب الفصول - komurasoft-blog-samples (GitHub)
• SPARK - AdaCore
• Introduction to SPARK - learn.adacore.com
• SPARK 2014 Reference Manual
• GNATprove User’s Guide
• Ada Reference Manual (Ada 2022)
• Alire - Ada Library Repository
• Why3 - Platform for Deductive Program Verification
• جاذبيّة لغة Ada ── لغة تعبّر عن التصميم بالأنواع وتسند برمجيّات تعمل لعقود - هذا الموقع

مقالات ذات صلة

أحدث المقالات التي تشترك في نفس الوسوم. عمّق فهمك بمواضيع مرتبطة.

الأسئلة الشائعة

أسئلة شائعة حول موضوع هذه المقالة.

ما هو SPARK؟ وما علاقته بـ Ada؟

SPARK مجموعة فرعيّة (لغة جزئيّة) من Ada، صُمِّمت بحيث يمكن إثبات خصائص البرنامج رياضيّاً. تقيّد الإدارة الديناميكيّة للذاكرة عبر المؤشّرات والاستخدام الحرّ للاستثناءات مقابل الحصول على قابليّة الإثبات. شيفرة SPARK هي شيفرة Ada مضافاً إليها تعليقات العقود، لذا فهي امتداد لتطوير Ada المعتاد ولا تحتاج إلى إعادة تعلّم صياغة خاصّة. محور الأدوات هو GNATprove من AdaCore: يحوّل العقود إلى اللغة الوسيطة Why3 ويحاول الإثبات بمُثبِتات آليّة مثل Z3.

ما الفرق بين التحقّق الشكلي والاختبار؟

يتحقّق الاختبار من أنّ البرنامج يعمل بشكل صحيح للمدخلات المختارة، بينما يُثبت التحقّق الشكلي رياضيّاً أنّ الخاصيّة تتحقّق لكلّ المدخلات. تركيبات المدخلات غير محدودة، لذا لا يُظهر الاختبار وحده الصحّة على كلّ المدخلات. الأسلوبان لا يتعارضان بل يكمّلان بعضهما: المزيج العمليّ هو ضمان مستوى Silver في SPARK (غياب أخطاء وقت التشغيل)، والتحقّق من مدخلات ومخرجات محدَّدة باختبارات الوحدة، وتركيز الاختبار على الأجزاء التي يتعذّر إثباتها.

ما هي مستويات البرهان في SPARK (من Stone إلى Platinum)؟

مفهوم لرفع صرامة البرهان تدريجيّاً. Stone يؤكّد أنّ الشيفرة SPARK صالحة، وBronze يثبت عدم قراءة متغيّرات غير مُهيَّأة وصحّة تدفّق البيانات، وSilver يثبت عدم وقوع أخطاء وقت التشغيل (خارج النطاق، وتجاوز السعة، والقسمة على صفر). Gold يضيف إلى ذلك إثبات خصائص نزاهة (integrity) أساسيّة، مثل بقاء ثوابت بيانات مهمّة أو أنّ انتقال الحالة يطابق المواصفة. Platinum مستوى صحّة وظيفيّة كاملة يثبت أنّ العقود تغطّي المتطلّبات الوظيفيّة وأنّ التنفيذ يطابق المواصفة؛ تكلفته مرتفعة وأمثلة الوصول إليه قليلة. في العمل الفعليّ يُعدّ استهداف Silver أوّلاً الهدف الأكثر واقعيّة.

ماذا أفعل عندما يتعذّر الإثبات في GNATprove؟

عالج الرسائل واحدة واحدة. «postcondition might fail» يعني أنّ شرط Post أقوى من اللازم أو شرط Pre أضعف من اللازم، أو أنّ ثابت الحلقة ناقص. «overflow check might fail» يُعالَج بتضييق مدى القيمة في Pre أو بتضييق مدى النوع نفسه. «array index check might fail» يُعالَج بإظهار أنّ مدى الحلقة داخل مدى المصفوفة عبر ثابت. «prover timeout» يُعالَج بتقسيم البرهان تدريجيّاً بالثوابت أو بتصغير الدوالّ. أوّل خطوة هي قراءة الشيفرة والحكم إن كان الفشل ممكناً فعلاً.

الملف الشخصي للمؤلف

صفحة الملف الشخصي لمؤلف المقالة.

غو كومورا

مؤسّس شركة كومورا سوفت ذ.م.م.

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