تُبين هذه الورقة أن الدلالات البديهية القائمة على منطق هوار تقبل نماذج غير معيارية تشبه نماذج سكولم، مما يؤدي إلى فشلها في تعريف الدلالات التشغيلية بشكل فريد، وتقترح إثراء النظام بالتزامات إثبات إضافية لحل هذا الغموض دون التأثير على نماذج التتبع المعيارية.
في عالم علوم الحاسوب، هناك توتر مستمر بين كيفية وصفنا لما يجب أن يفعله البرنامج وكيفية إثبات أنه يفعل ذلك بالفعل. لعقود من الزمن، اعتمد الباحثون على نظام يسمى "منطق هوار" (Hoare logic) للتحقق من البرمجيات. يعمل هذا النظام كطقم من القواعد المنطقية: إذا بدأ البرنامج في حالة معينة، واستطعنا إثبات أنه يتبع خطوات محددة، فإنه لا بد أن ينتهي في الحالة المنشودة. إنه أداة قوية لضمان خلو الكود من الأخطاء، تماماً كما يضمن البرهان الرياضي صحة نظرية ما. ومع ذلك، تماماً كما اكتشف علماء الرياضيات ذات يوم أن قواعدهم لعد الأرقام يمكن أن تصف بالخطأ عوالم غريبة ومستحيلة، وجد علماء الحاسوب أن قواعد التحقق من البرامج قد تصف أيضاً طرقاً مستحيلة لتشغيل الكود. والسؤال هو ما إذا كان المنطق الذي نستخدمه للوثوق ببرمجياتنا دقيقاً بما يكفي لاستبعاد هذه السيناريوهات المستحيلة.
لقد أظهر باحث في جامعة نيويورك مؤخاً أن القواعد القياسية للتحقق من البرامج فضفاضة للغاية بالفعل. فقد أثبت أن المنطق المستخدم لإثبات صحة البرامج يسمح بنماذج تنفيذ "غير قياسية". وببساطة، يعني هذا أن القواعد تسمح للبرنامج بأن يعمل بطرق ممكنة رياضياً ضمن المنطق، ولكنها مستحيلة فيزيائياً في العالم الحقيقي. تخيل برنامجاً يعد تصاعدياً إلى ما لا نهاية؛ الرؤية القياسية هي أنه يبدأ من الصفر وينتقل إلى واحد، اثنان، ثلاثة، وهكذا، دون توقف. ومع ذلك، فإن المنطق يسمح أيضاً بنسخة من هذا البرنامج تكون قد عملت لفترة زمنية لانهائية في الماضي قبل أن نبدأ بمراقبته، أو نسخة موجودة في خط زمني ممتد وغريب لا يتوافق مع فهمنا الطبيعي للزمن. لقد أثبت الباحث أن المنطق الحالي لا يستطيع التمييز بين السلوك المتوقع والمنطقي للبرنامج وبين هذه السلوكيات غير القياسية والغريبة. وهذا يمثل مشكلة كبيرة لأنه إذا كان المنطق لا يستطيع التمييز بين العالم الحقيقي والعوالم المستحيلة، فإنه لا يحدد بشكل فريد ما يفعله البرنامج بالفعل.
لفهم سبب حدوث ذلك، يجب النظر في كيفية التحقق من الحلقات التكرارية (loops) في برامج الحاسوب. عندما يكرر البرنامج كتلة من الكود، مثل حلقة تعمل طالما كان الشرط صحيحاً، يتطلب المنطق وجود "ثابت للحلقة" (loop invariant). وهذا الثابت هو عبارة تظل صحيحة في كل مرة تتكرر فيها الحلقة. وقد أظهر الباحث أنه بالنسبة للعديد من البرامج، يمكنك ابتكار ثابت للحلقة يكون صحيحاً للتنفيذ القياسي والطبيعي للكود، ولكنه يكون صحيحاً أيضاً لهذه التنفيذات غير القياسية والغريبة. على سبيل المثال، لننظر في برنامج يعد تصاعدياً؛ يسمماح المنطق ببرهان يعمل لعد يبدأ من الصفر ويتجه للأعلى، ولكنه يسمح أيضاً ببرهان يعمل لعد يتحرك تراجعياً من سالب ما لا نهاية، أو لعد موجود في خط زمني يحتوي على خطوات إضافية غير مرئية لا يمكن للبشر إدراكها. ولأن المنطق يعامل هذه الخطوط الزمنية المختلفة كأنها صالحة، فإنه يفشل في تحديد معنى واحد وفريد للبرنامج. إن المنطق هنا غامض، تماماً مثل تعريف قديم للأرقام سمح بوجود "أرقام شبحية" تتصرف مثل الأرقام العادية ولكنها ليست جزءاً من تسلسل العد القياسي.
لا يكتفي البحث بتحديد هذا الغموض فحسب، بل يقدم طريقة لإصلاحه. يقترح الباحث إضافة متطلبات إضافية إلى عملية التحقق، مستوحاة من الأساليب المستخدمة لإثبات أن البرنامج سيتوقف عن العمل في النهاية. تعمل هذه المتطلبات الجديدة كمرشح (فلتر)؛ فهي تفرض أن إثبات صحة البرنامج يجب أن يظهر أيضاً أن تنفيذ البرنامج يتبع مساراً قياسياً محدداً عبر الزمن. وتحديداً، تتطلب القواعد الجديدة أنه إذا كنت تعد خطوات حلقة تكرارية، فيجب أن يتبع العد التقدم القياسي للأرقام التي نستخدمها يومياً، دون أي امتدادات لانهائية خفية. وإذا كان سلوك البرنامج يعتمد على تلك الخطوط الزمنية غير القياسية الغريبة، فإن القواعد الجديدة ستفشل في إثبات صحته. وهذا يؤدي فعلياً إلى إجبار المنطق على تجاهل العوالم المستحيلة والتركيز فقط على التنفيذات القياسية والواقعية التي تهمنا.
والأهم من ذلك، أن الباحث يوضح أنه بالنسبة لأي برنامج يعمل بشكل طبيعي، فإن هذه المتطلبات الجديدة يتم استيفاؤها تلقائياً. وهذا يعني أن الغالبية العظمى من أعمال التحقق من البرمجيات التي يقوم بها الناس اليوم تظل براهينها صالحة ودون تغيير. القواعد الجديدة لا تجعل مهمة إثبات صحة البرامج أصعب في الحالات القياسية؛ بل تقوم ببساطة بإغلاق الباب الخلفي الذي سمح للحالات المستحيلة بالتسلل. والنتيجة هي تعريف أكثر دقة لما يعنيه البرنامج. ومن خلال إضافة هذه الفحوصات الإضافية، يصبح المنطق أخيراً وصفاً فريداً لسلوك البرنامج، مما يضمن أننا عندما نقول إن برنامجاً ما صحيح، فإننا نتحدث عن طريقة واحدة محددة لتشغيله، وليس مجموعة من الاحتمالات التي تشمل بعضها واقعاً يتحدى فهمنا للزمن والتسلسل.
يربط هذا العمل بين مشكلة عميقة في أسس الرياضيات والمهمة العملية لكتابة برمجيات آمنة. تماماً كما قام علماء الرياضيات ذات يوم بتنقيح تعريفهم للأرقام لاستبعاد التباينات المستحيلة، يقوم هذا البحث بتنقيح تعريف تنفيذ البرنامج. إنه يضمن أن الأدوات التي نستخدمها للتحقق من سلامة الأنظمة الحرجة ليست متسقة منطقياً فحسب، بل هي أيضاً راسخة في الواقع القياسي الوحيد لكيفية عمل الحواسيب فعلياً. الحل أنيق لأنه لا يتطلب إعادة كتابة النظام بأكمله للتحقق من البرامج؛ بل يضيف ببساطة حاجز حماية يبقي المنطق على المسار المقصود، مما يضمن أن ثقتنا في البرمجيات مبنية على حقيقة فريدة ومعرفة جيداً.
ملخص تقني: الدلالات البديهية غير القياسية
بيان المشكلة
تتناول الورقة غموضًا جوهريًا في الدلالات البديهية القائمة على منطق هوار (Hoare logic). وعلى غرار نماذج سكولم (Skolem) غير القياسية لحساب بيانو، يوضح المؤلف أن منطق هوار يسمح بوجود نماذج غير قياسية لتنفيذ البرامج. وتحديدًا، لا يحدد المنطق بشكل فريد الدلالات التشغيلية المقصودة (دلالات المسارات/trace semantics) للغات البرمجة حتى مع مراعاة التماثل (isomorphism).
تنشأ المشكلة الجوهرية في قاعدة التكرار (Rule of Iteration). فبينما يستخدم منطق هوار الثوابت الاستقرائية (inductive invariants) للاستدلال على الحلقات التكرارية، فإن نظرية المنطق القياسية لا تستطيع التمييز بين:
المسارات غير القياسية (Nonstandard traces): التنفيذات المفهرسة بأعداد طبيعية غير قياسية (مثل نماذج سكولم التي تحتوي على "ماضٍ لانهائي" أو "مستقبل لانهائي" يتجاوز ω القياسية).
وبناءً على ذلك، فإن إثبات منطق هوار الذي يكون صحيحًا لنموذج مسار قياسي يكون أيضًا صحيحًا للنماذج غير القياسية حيث يمكن أن تكون أطوال الحلقات التكرارية غير قياسية (مثل البدء من ماضٍ غير قياسي أو الاستمرار في مستقبل غير قياسي). وهذا يعني أن منطق هوار، كما تمت صياغته تقليديًا، لا يحدد دلالات تشغيلية فريدة ومعرفة جيدًا.
المنهجية
يستخدم المؤلف تحليلًا مقارنًا بين دلالات المسار القياسية ودلالات المسار غير القياسية، مستفيدًا من مفاهيم التجريد (abstract interpretation) ونظرية النقطة الثابتة (fixpoint theory).
الدلالات القياسية: تُعرف عبر النقطة الثابتة الصغرى ($lfp)والنقطةالثابتةالكبرى(gfp)علىشبكةالمساراتالمتناهية(\Sigma^*)واللانهائية(\Sigma^\infty)المفهرسةبـ\mathbb{N}$.
الدلالات غير القياسية: تمتد إلى المسارات المفهرسة بمجموعات غير قياسية مثل N+δ (مسارات أمامية غير قياسية ذات مستقبل لانهائي) و N−δ (مسارات خلفية غير قياسية ذات ماضٍ لانهائي)، حيث δ>0. وتمثل هذه المجموعات هياكل شبيهة بنماذج سكولم.
يثبت النظرية 1 أن مجموعة ثلاثيات هوار الصحيحة للدلالات القياسية (H(L)) هي نفسها مجموعة الثلاثيات الصحيحة للدلالات غير القياسية (H~(L)). وهذا يؤكد أن قواعد إثبات هوار القياسية غير كافية لاستبعاد التفسيرات غير القياسية.
العلاج المقترح (التقييس/Standardisation): لحل هذا الغموض، يقترح المؤلف إثراء الدلالات البديهية بالتزامات إثبات إضافية مستوحاة من طرق إثبات الإنهاء (تحديدًا طريقة كنوت/Knuth والمتغيرات الرتبوية/ordinal variants).
منع المسارات الأمامية غير القياسية: يتم توسيع المنطق ليتطلب وجود دالة متزايدة K تربط مواضع المسار بالرتب (ordinals O) بحيث يكون عداد الحلقة محصورًا بـ أول حد لانهائي رتبي ω. وبما أن الأجزاء الصحيحة غير القياسية لا يمكن أن تكون متماثلة رتبيًا مع الأعداد الرتبية جيدة التأسيس (well-founded ordinals)، فإن هذا المتطلب يقضي على المسارات الأمامية اللانهائية غير القياسية.
منع المسارات الخلفية غير القياسية: يتم تقديم متطلب مزدوج للمسارات الخلفية، يتطلب دالة متناقصة K (antitone) تضمن أن التتبع الخلفي ينتهي ضمن حد قياسي.
المساهمات الرئيسية
تحديد النماذج غير القياسية: تثبت الورقة رسميًا أن منطق هوار يعاني من مشكلة عدم التفرد نفسها التي يعاني منها حساب بيانو دون شرط ديديكيند (Dedekind's categoricity condition). وتوضح أن ثوابت الحلقات في المنطق من الدرجة الأولى لا تستطيع التمييز بين نماذج المسارات القياسية وغير القياسية بسبب نظرية التراص (compactness theorem).
تكافؤ النظريات: تثبت الورقة أن نظريات منطق هوار القياسية وغير القياسية متطابقة (H(L)=H~(L))، مما يعني أن الإثباتات الموجودة لا تستبعد بطبيعتها التنفيذات غير القياسية.
التقييس عبر القيود الرتبية: تقترح الورقة طريقة لتقييد الدلالات البديهية بالنماذج القياسية عن طريق إضافة التزامات إثبات تتضمن عدادات رتبية (مقيدة بـ ω للمسارات الأمامية وتتطلب الإنهاء للمسارات الخلفية).
الحفاظ على الإثباتات القياسية: النتيجة الحاسمة هي أن هذه الالتزامات الإضافية للإثبات محققة دائمًا بواسطة دلالات المسار القياسية. لذلك، إذا افترضنا التفسير القياسي (كما هو ضمني في معظم استخدامات منطق هوار)، فإن إثباتات هوار الحالية تظل صحيحة ولا تتغير. تعمل الالتزامات الجديدة على استبعاد النماذج غير القياسية رسميًا دون تغيير التحقق العملي من البرامج القياسية.
النتائج
التكافؤ النظري: مجموعة ثلاثيات هوار الصحيحة لنماذج المسار غير القياسية هي بالضبط نفس المجموعة الخاصة بالنماذج القياسية.
حل الغموض: من خلال فرض شروط الحد الرتبي (المعادلتان 9 و10)، يتم تقييد الدلالات البديهية بالنموذج القياسي.
القابلية للتطبيق: التقييس المقترح متوافق مع خوارزميات التحليل الساكن وأنواع البيانات التي تعتمد على منطق هوار، بشرًا ما يتم جعل افتراض الدلالات القياسية صريحًا أو يتم التحقق من الالتزامات الجديدة (وهو أمر بديهي للنماذج القياسية).
المحددات: تشير الورقة إلى أنه في منطق هوار المجرد (Abstract Hoare Logics)، حيث يتم استبدال المجال الملموس بمجال مجرد قد لا يكون معبرًا بما يكفي لتعريف الدوال الرتبية المطلوبة، قد لا تكون طرق التقييس قابلة للتطبيق بشكل مباشر.
الأهمية
تجادل الورقة بأن الادعاء الشائع بأن "الدلالات البديهية تحدد معنى البرنامج من خلال تأثيراتها على التأكيدات المنطقية" هو ادعاء معيب تقنيًا لأن المعنى المحدد ليس فريدًا من حيث التماثل (isomorphism). تكمن الأهمية في:
توضيح الأسس: فهي تسلط الضوء على أن منطق هوار، مثل حساب بيانو، يتطلب شرط "التقطعية" (categoricity) (في هذه الحالة، التقييس عبر الحدود الرتبية) لضمان تفسير تشغيلي فريد.
صياغة الافتراضات الضمنية: إنها تجعل الفرضية الضمنية التي تقول بأن منطق هوار يُفسر فوق نماذج حساب قياسية فرضية صريحة.
الربط بين المنطق والدلالات: توضح كيف يمكن دمج تقنيات إثبات الإنهاء (باستخدام الرتب) في الدلالات البديهية لاستبعاد التفسيرات غير القياسية، مما يؤدي إلى مواءمة الدلالات البديهية بشكل أكثر صرامة مع دلالات المسار التشغيلية.
تخلص المؤلفة إلى أنه بينما لا تحتاج إثباتات منطق هوار إلى التغيير بالنسبة للنماذج القياسية، إلا أن الإطار النظري يجب أن يعترف بالنماذج غير القياسية ويستبعدها رسميًا للمطالبة بتعريف فريد لدلالات البرنامج.