منطق هور

قاعدة while للصحة الكلية

ويمكن إثبات ذلك على النحو التالي:

علاوةً على ذلك، وبما أن مؤسسة جيدًا، فإن أي تسلسل تناقصي صارم لمتغيرات من يكون نهائيًا؛ فلا يمكن أن يستمر في التناقص إلى الأبد. (مثلًا، الترتيب الاعتيادي مؤسَّس جيدًا على الأعداد الصحيحة الموجبة ، لكنه ليس كذلك على ولا على ؛ وكل هذه المجموعات تُفهم بالمعنى الرياضي لا الحاسوبي، وهي جميعًا لانهائية).

من جانب آخر، وبتعبير غير رسمي، يجب إثبات أن المسافة تتناقص في كل دورة من الحلقة، بينما تظل غير سالبة؛ مما يعني أن هذه العملية لا يمكن أن تستمر إلا لعدد محدود من الدورات.

وعلى صعيد آخر، إذا تم استبدال قاعدة while العادية أعلاه بالقاعدة التالية، يمكن استخدام حساب هور لإثبات الصحة الكلية، أي التوقف إلى جانب الصحة الجزئية. وغالبًا ما تُستعمل الأقواس المربعة بدلاً من المعقوفة للإشارة إلى المفهوم المختلف لصحة البرامج:

• انظر كذلك
• ملاحظات
• المراجع
• البيبليوغرافيا

يمكن تبسيط هدف الإثبات السابق إلى:

يتم الحصول عليها باستخدام قاعدة الإسناد،

،

كذلك، في هذه القاعدة، إلى جانب الحفاظ على ثبات الحلقة، يجب كذلك إثبات إثبات التوقف عبر تعبير يُعرف باسم متغيّر الحلقة، الذي تتناقص قيمته تناقصًا صارمًا وفق علاقة ترتيب مؤسَّسة جيدًا على مجموعة خلال كل تكرار.

في هذا الإطار، يمكن تطبيق قاعدة while للصحة الكلية باختيار كالأعداد الصحيحة غير السالبة مع الترتيب الاعتيادي، والتعبير كـ ، مما يتطلب بدوره إثبات:

علاوةً على ذلك، وبالرجوع إلى المثال الأول في القسم السابق، لإثبات الصحة الكلية لـ

وفي هذا الصدد، بما أن هو ثبات الحلقة، يجب أن يُشير الشرط إلى أن ليس عنصرًا عنصرًا أدنى في ؛ وإلا فلن يتمكن جسم الحلقة من إنقاص أكثر، أي أن مقدم القاعدة سيكون خاطئًا. (هذه إحدى صيغ الصحة الكلية.)

ويمكن تقويتها إلى باستخدام قاعدة النتيجة.

وعلى صعيد آخر، في المثال الثاني من القسم السابق، من الواضح أنه لا يمكن العثور على أي تعبير يتم إنقاصه بواسطة جسم الحلقة الفارغ، وبالتالي لا يمكن إثبات الانتهاء.

قاعدة العاقبة

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

ومع ذلك، بما أن العبارة

فإنه يمكن اشتقاق قاعدة الشرط من قواعد هور الأخرى.

لها نفس تأثير البنية التكرارية لمرة واحدة التالية:

كذلك، وبطريقة مشابهة، يمكن تحويل القواعد الخاصة ببنى البرامج الأخرى المشتقة، مثل حلقة ، وحلقة ، وتعليمة ، و، و من خلال تحويل البرنام إلى القواعد الموجودة في ورقة هور الأصلية.

قاعدة الشرطية

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

لم تكن هذه القاعدة واردة في منشور هور الأصلي.

ومن جهة أخرى، يجب ألّا تُحدِث الشرط أي تأثيرات جانبية. يُقدَّم مثال في القسم التالي.

، أو مبسطة

كذلك، في الواقع، هذا البرنامج الغريب صحيح جزئيًا فقط: إذا انتهى تنفيذه، فهذا يعني أن قد احتوى صدفةً على الجذر التربيعي لـ .

وأخيراً، يمكن تبسيط الشرط اللاحق إلى .

،

،

بعد تطبيق قاعدة while مع كون هو ، يتبقى إثبات:

وهو ما ينتج عن قاعدة التجاوز (skip) وقاعدة العاقبة.

وعلى صعيد آخر، كمثال آخر، يمكن استخدام قاعدة while للتحقق رسميًا من البرنامج الغريب التالي لحساب الجذر التربيعي الدقيق لعدد عشوائي —حتى لو كانت متغيرًا صحيحًا و عددًا غير مربعي:

وهو ما يُستنتج بسهولة من قاعدة الإسناد.

أما في الحالات الأخرى، فلن ينتهي؛ لذا فهو ليس صحيحًا كليًا.

، أو مبسطة

لجزء .

من جانب آخر، ومع ذلك، تتطلب قاعدة الإسناد في جزء اختيار كـ ؛ وبالتالي تطبيق القاعدة يُعطي:

الثلاثية بحسب هور

وفي هذا السياق، يوفر منطق هور مسلمات وقواعد استدلال لجميع بنيات البرمجة الأمرية البسيطة. إلى جانب القواعد المتعلقة باللغة البسيطة في ورقة هور الأصلية، فقد طُوّرت لاحقًا قواعد لبنيات لغوية أخرى من قِبل هور وغيرِه من الباحثين. وتشمل هذه القواعد ما يتعلق بـالتزامن، والدوال، وأوامر القفز، والمؤشرات.

من جانب آخر، حيث و هما عبارتان شرطيّتان و هو أمر برمجي. تُسمّى الشرط القبلي و الشرط البعدي: فعندما يتحقق الشرط القبلي، فإن تنفيذ الأمر يؤدي إلى تحقق الشرط البعدي. العبارات الشرطية هي صيغ في منطق الرتبة الأولى.

في هذا الإطار، الميزة المركزية في منطق هور هي ثلاثية هور، وهي تصف كيف تُغيّر قطعة من الشيفرة حالة الحوسبة بعد تنفيذها. تكون ثلاثية هور على الشكل:

قاعدة العملية الفارغة

من جانب آخر، تؤكد قاعدة العملية الفارغة أن التعليمة لا تُغيّر حالة البرنامج، لذا فإن أي شرط يتحقق قبل سيبقى محققًا بعدها.

الصحة الجزئية والصحة الكلية

وفي هذا السياق، مصطلح "الإنهاء" هنا وفي باقي المقال يُفهم بالمعنى الأوسع: أن تنتهي الحوسبة في نهاية المطاف، أي أنه لا توجد حلقات لا نهائية؛ ولا يُشترط غياب أخطاء التنفيذ (مثل القسمة على صفر) التي قد توقف البرنامج مبكرًا. في ورقته عام 1969، استعمل هور تعريفًا أضيق للإنهاء يتضمن كذلك غياب انتهاكات حدود التنفيذ، وقد أعرب عن تفضيله للتعريف الأوسع لأنه يجعل العبارات الشرطية مستقلة عن تفاصيل التنفيذ:

إضافةً إلى ذلك، باستخدام منطق هور القياسي، يمكن إثبات الصحة الجزئية فقط. أما الصحة الكلية، فهي تتطلب علاوةً على ذلك إثبات الإنهاء، والذي يمكن إثباته بشكل منفصل أو باستخدام نسخة موسعة من قاعدة التكرار While. بالتالي، التفسير البديهي لثلاثية هور هو: كلما تحقق من الحالة قبل تنفيذ ، فإن سيتحقق بعد التنفيذ، أو أن لن ينتهي. في الحالة الأخيرة، لا توجد "نهاية"، لذا يمكن أن تكون أي عبارة كانت. في الواقع، يمكن اختيار لتكون خاطئة للتعبير عن أن لا ينتهي.

القواعد

، أو مكافئة

،

ومن جهة أخرى، لذلك يجب تطبيق قاعدة العاقبة بحيث يكون و هما و على التوالي، لتقوية الشرط المسبق مرة أخرى. وبتعبير غير رسمي، فإن تأثير قاعدة العاقبة هو "نسيان" أن كان معلوماً عند دخول جزء ، لأن قاعدة الإسناد المستعملة لذلك الجزء لا تحتاج إلى هذه المعلومة.

قاعدة التركيب

مثال:

التسلسل يعطي:

وفي هذا السياق، تنطبق قاعدة التركيب على برنامجين ينفّذان بالتسلسل، ثم ، ويُكتب ذلك ، حيث تُدعى بـ"الشرط الوسيط":

قاعدة while

• وكما في قاعدة الشرط، يجب ألا يُحدِث أي تأثيرات جانبية.
• مثلًا، لإثبات:
• باستخدام قاعدة while، يجب إثبات:

علاوةً على ذلك، بعد انتهاء الحلقة، يظل هذا الثبات قائمًا، ويجب كذلك أن تكون قد تسببت في إنهاء الحلقة.

هنا، هو ثبات الحلقة، الذي يجب الحفاظ عليه داخل جسم الحلقة .

قاعدة الإسناد

أمثلة على ثلاثيات صحيحة:

تكون غير صحيحة إذا كان كل من و يشيران لنفس الموقع.

كذلك، العبارات القبلية غير المتأثرة بالإسناد يمكن نقلها إلى العبارة البعدية. مثلًا، في المثال الأول، لا يتغير بعد تنفيذ .

علاوةً على ذلك، لكن هذه القاعدة لا تصح عندما يشير أكثر من اسم إلى نفس المكان في الذاكرة (كما في حالة الإشارة المشتركة). مثلًا:

في هذا الإطار، هذا يعني أن تحقق قبل الإسناد يعادل تحقق بعده. فلو كانت صحيحة قبل الإسناد، فإن ستكون صحيحة بعده، والعكس غير صحيح بالضرورة.

من جهة ثانية، تنص قاعدة الإسناد على أنه بعد تنفيذ الإسناد، فإن أي تعبير كان محققًا لجهة اليمين من الإسناد، سيتحقق للمتغير المُسنَد إليه. لنفترض أن عبارة شرطية تحتوي على المتغير كمُتغير حر. إذًا:

ومن ناحية أخرى، حيث تعني العبارة الشرطية بعد استبدال كل ظهور حر للمتغير بالتعبير .

، وهو ما يعادل منطقياً

وبالمثل، لجزء ، تعطي قاعدة الإسناد:

.

كذلك، وبالتالي، تُستعمل قاعدة العاقبة لتقوية الشرط المسبق المستنتج من قاعدة الإسناد إلى المطلوب لقاعدة الشرط.