شركة كومورا سوفت ذ.م.م.
تواصل معنا
القائمة

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

· · Ada, SPARK, التحقق الشكلي, GNATprove, التصميم بالعقد, النزاهة العالية, لغة برمجة, الموثوقية العالية

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

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

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

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

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

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

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

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

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

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

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

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

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 وCVC4 وAlt-Ergo
4. الإبلاغ عن النتائج كرسائل مباشرة على الشيفرة المصدريّة

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

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

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

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

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

باستخدام 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.

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_Type)
  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 Levels).

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

Stone (المستوى 0):
  فحص صياغة العقود واتّساق الأنواع فقط
  أوّل مستوى ينبغي بلوغه

Bronze (المستوى 1):
  Stone + إثبات عدم قراءة متغيّرات غير مُهيَّأة
  ضمان الصحّة الأساسيّة

Silver (المستوى 2):
  Bronze + إثبات خلوّ البرنامج من أخطاء التشغيل (تجاوز الحدود،
  وتجاوز السعة، والقسمة على صفر)
  الهدف الأكثر واقعيّة

Gold (المستوى 3):
  Silver + إثبات شرطَي Pre/Post
  ضمان الصحّة الوظيفيّة الكاملة

Platinum (المستوى 4):
  Gold + إثبات استقلاليّة البيانات وتدفّق المعلومات
  للأنظمة التي تُعطي الأولويّة للأمان

استراتيجيّة تبنٍّ عمليّة:

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

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

المرحلة 3: إثبات المنطق الأساسيّ عند مستوى Gold
  → ضمان الصحّة الوظيفيّة رياضيّاً
  → إثبات صحّة الخوارزميّات

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

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

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

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

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

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

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

5. راجع التحذيرات ونقِّح العقود عند الحاجة
   انتبه بشكل خاصّ لمشاكل التهيئة

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

7. أضف ثوابت الحلقات حيث يلزم
   إن فشل البرهان، تحقّق ممّا إذا كانت الثوابت ناقصة

8. أثبت الصحّة الوظيفيّة عند مستوى Gold
   gnatprove -P proj.gpr --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 (البرهان الوظيفيّ الكامل) مثاليّ، لكن ابدأ بـ 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، ستتغيّر نظرتك إلى ضمان جودة البرمجيّات.

مراجع

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

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

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

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

ما هو SPARK؟ وما علاقته بـ Ada؟
SPARK هو مجموعة فرعيّة (subset) من Ada مقيَّدة عن قصد، صُمِّمت بحيث يمكن إثبات خصائص البرنامج رياضيّاً. يحدّ SPARK من الميزات الصعبة التحقّق منها ── الاستخدام الحرّ للمؤشّرات (pointers)، والمعالجة غير المقيَّدة للاستثناءات، وبِنى البيانات المتكرّرة (recursive)، والاستخدام غير المقيَّد للمهامّ (tasking) ── مقابل الحصول على قابليّة الإثبات. شيفرة SPARK هي شيفرة Ada مضافاً إليها توضيحات العقود (contract annotations)، لذا فهي امتداد طبيعيّ لتطوير Ada المعتاد وليست لغة مختلفة. أداة GNATprove من AdaCore هي محور الأدوات، إذ تترجم العقود إلى اللغة الوسيطة Why3 وتحاول إثباتها باستخدام مُثبِتات آليّة مثل Z3 وCVC4 وAlt-Ergo.
ما الفرق بين التحقق الشكلي باستخدام SPARK والاختبار (testing)؟
يتحقّق الاختبار من أنّ البرنامج يعمل بشكل صحيح للمدخلات المُختارة، بينما يُثبت التحقق الشكلي رياضيّاً أنّ خاصيّة ما تتحقّق لكلّ المدخلات الممكنة. الأسلوبان لا يتعارضان بل يكمِّلان بعضهما: SPARK يُثبت فقط الخصائص المكتوبة في العقود، بينما يمكن للاختبار أن يكشف افتراضات ضمنيّة لم تُدوَّن قطّ، وأن يتحقّق من التفاعل مع بيئة التشغيل. المزيج العمليّ هو ضمان خلوّ البرنامج من أخطاء التشغيل باستخدام SPARK (مستوى Silver)، والتحقّق من سلوك مدخلات ومخرجات محدَّدة باختبارات الوحدة (unit tests)، وتركيز الاختبار على الأجزاء التي يتعذّر إثباتها.
ما هي مستويات البرهان في SPARK (من Stone إلى Platinum)، وأيّها ينبغي استهدافه أوّلاً؟
يحدّد SPARK خمسة مستويات متزايدة الصرامة: Stone (فحص صياغة العقود واتّساق الأنواع)، وBronze (يضيف إثبات عدم قراءة متغيّرات غير مُهيَّأة)، وSilver (يضيف إثبات خلوّ البرنامج من أخطاء التشغيل مثل تجاوز السعة، وتجاوز الحدود، والقسمة على صفر)، وGold (يضيف إثبات الصحّة الوظيفيّة عبر شرطَي Pre/Post)، وPlatinum (يضيف استقلاليّة البيانات وإثبات تدفّق المعلومات). مستوى Silver هو الهدف الأوّل الأكثر واقعيّة ── إذ تُستبعَد معظم الأخطاء الحقيقيّة بمجرّد التخلّص من أخطاء التشغيل ── بينما يستحقّ مستوى Gold السعي إليه في المنطق الأساسيّ الذي يجب ضمان صحّته.
ما هو ثابت الحلقة (loop invariant)؟ ولماذا تحتاج إثباتات SPARK إليه؟
ثابت الحلقة هو خاصيّة تتحقّق في بداية كلّ تكرار (iteration) من الحلقة، وتُكتب باستخدام pragma Loop_Invariant. تُنفَّذ الحلقات عدداً غير محدَّد من المرّات، لذا يحتاج المُثبِت إلى الثابت كي يستدلّ على كلّ التكرارات دفعة واحدة ── فهو يعبّر عن الحساب الجزئيّ المُنجَز حتّى تلك النقطة في صورة صيغة رياضيّة، ويجب أن يستلزم بعد آخر تكرار الشرط اللاحق (postcondition) المطلوب. تصميم الثوابت هو أدقّ مهارة في إثبات الحلقات: فالثابت الأقوى من اللازم يتعذّر إثباته، والأضعف من اللازم لا يستلزم الشرط اللاحق.

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

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

غو كومورا

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

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

تواصل معنا

روابط عامة

GitHub LinkedIn X COM_BLAS COM_BigDecimal
العودة إلى المدونة