منطق هور

**منطق هور** (المعروف أيضًا باسم **منطق فلويد–هور** أو **قواعد هور**) هو نظام شكلي يحتوي على مجموعة من القواعد المنطقية للتفكير بشكل دقيق حول صحة برامج الكمبيوتر. تم اقتراحه في عام 1969 بواسطة عالم الكمبيوتر البريطاني والمنطق الرياضي توني هور، ثم تم تحسينه لاحقًا من قبل هور وباحثين آخرين. كانت الأفكار الأصلية قد بدأت بعمل روبرت فلويد، الذي نشر نظامًا مشابهًا للمخططات الانسيابية.

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

: \{P\} C \{Q\}

حيث P وQ هما *[[assertion (computing)|عبارتان شرطيّتان]]* وC هو *أمر برمجي*. تُسمّى P *[[الشرط القبلي]]* وQ *[[الشرط البعدي]]*: فعندما يتحقق الشرط القبلي، فإن تنفيذ الأمر C يؤدي إلى تحقق الشرط البعدي. العبارات الشرطية هي صيغ في منطق الرتبة الأولى.

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

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

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

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

## القواعد

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

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

: \dfrac{}{\{P\}\texttt{skip}\{P\}}

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

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

: \dfrac{}{\{P[E/x]\} x := E \{P\}}

حيث P[E/x] تعني العبارة الشرطية  بعد استبدال كل ظهور حر للمتغير  بالتعبير .

هذا يعني أن تحقق P[E/x] قبل الإسناد يعادل تحقق  بعده. فلو كانت P[E/x] صحيحة قبل الإسناد، فإن  ستكون صحيحة بعده، والعكس غير صحيح بالضرورة.

أمثلة على ثلاثيات صحيحة:
:* \{ x+1 = 43 \}   y := x + 1   \{ y = 43 \}
:* \{ x + 1 \leq N \}  x := x  + 1  \{ x \leq N \}

العبارات القبلية غير المتأثرة بالإسناد يمكن نقلها إلى العبارة البعدية. مثلًا، في المثال الأول، لا يتغير x+1=43 بعد تنفيذ y:=x+1.

لكن هذه القاعدة لا تصح عندما يشير أكثر من اسم إلى نفس المكان في الذاكرة (كما في حالة الإشارة المشتركة). مثلًا:
: \{ y = 3 \}   x := 2   \{ y = 3 \}
تكون غير صحيحة إذا كان كل من  و يشيران لنفس الموقع.

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

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

:\dfrac{\{P\} S \{Q\}\quad,\quad   \{Q\} T \{R\}}{\{P\} S;T \{R\}}

مثال:

:\{ x + 1 = 43 \}   y := x + 1   \{ y = 43 \}

:\{ y = 43 \}   z := y   \{ z = 43 \}

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

:\{ x + 1 = 43 \}   y := x + 1; z := y   \{ z = 43 \}

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

:\dfrac{\{B \wedge P\} S \{Q\}\quad,\quad \{\neg B \wedge P \} T \{Q\}}{\{P\} \texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif} \{Q\}}

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

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

لم تكن هذه القاعدة واردة في منشور هور الأصلي.
ومع ذلك، بما أن العبارة
:\texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif}
لها نفس تأثير البنية التكرارية لمرة واحدة التالية:
:\texttt{bool}\ b:=\texttt{true};   \texttt{while}\ B\wedge b\ \texttt{do}\ S; b:=\texttt{false}\ \texttt{done};   b:=\texttt{true};   \texttt{while}\ \neg B\wedge b\ \texttt{do}\ T; b:=\texttt{false}\ \texttt{done}
فإنه يمكن اشتقاق قاعدة الشرط من قواعد هور الأخرى.
وبطريقة مشابهة، يمكن تحويل القواعد الخاصة ببنى البرامج الأخرى المشتقة، مثل حلقة ، وحلقة ، وتعليمة ، و، و من خلال تحويل البرنام إلى القواعد الموجودة في ورقة هور الأصلية.

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

:\dfrac{P_1 \rightarrow P_2\quad   ,\quad   \{P_2\} S \{Q_2\}\quad   ,\quad   Q_2 \rightarrow Q_1}{\{P_1\} S \{Q_1\}}

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

على سبيل المثال، لإثبات ما يلي:
:\{0 \leq x \leq 15 \}\texttt{if}\ x
يجب تطبيق قاعدة الشرط، والتي بدورها تتطلب إثبات:
:\{0 \leq x \leq 15 \wedge x ، أو مبسطة
:\{0 \leq x 
لجزء ، و
:\{0 \leq x \leq 15 \wedge x \geq 15\}   x:=0   \{0 \leq x \leq 15\}، أو مبسطة
:\{x=15\}   x:=0   \{0 \leq x \leq 15 \}
لجزء .

ومع ذلك، تتطلب قاعدة الإسناد في جزء  اختيار  كـ 0\leq x \leq 15؛ وبالتالي تطبيق القاعدة يُعطي:
:\{0 \leq x+1 \leq 15\}   x:=x+1   \{0 \leq x \leq 15\}، وهو ما يعادل منطقياً
:\{-1 \leq x .
وبالتالي، تُستخدم قاعدة العاقبة لتقوية الشرط المسبق \{-1 \leq x  المستنتج من قاعدة الإسناد إلى \{0 \leq x  المطلوب لقاعدة الشرط.

وبالمثل، لجزء ، تعطي قاعدة الإسناد:
:\{0 \leq 0 \leq 15\}   x:=0   \{0 \leq x \leq 15\}، أو مكافئة
:\{\texttt{true}\}   x:=0   \{0 \leq x \leq 15\}،
لذلك يجب تطبيق قاعدة العاقبة بحيث يكون P_1 وP_2 هما \{x=15\} و\{\texttt{true}\} على التوالي، لتقوية الشرط المسبق مرة أخرى. وبتعبير غير رسمي، فإن تأثير قاعدة العاقبة هو "نسيان" أن \{x=15\} كان معلوماً عند دخول جزء ، لأن قاعدة الإسناد المستخدمة لذلك الجزء لا تحتاج إلى هذه المعلومة.

### قاعدة while

:\dfrac{\{P \wedge B\} S \{P\}}{\{P\} \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} \{\neg B \wedge P\}}

هنا،  هو ثبات الحلقة، الذي يجب الحفاظ عليه داخل جسم الحلقة .
بعد انتهاء الحلقة، يظل هذا الثبات  قائمًا، ويجب أيضًا أن تكون \neg B قد تسببت في إنهاء الحلقة.
وكما في قاعدة الشرط، يجب ألا يُحدِث  أي تأثيرات جانبية.

على سبيل المثال، لإثبات:
:\{x \leq 10\} \texttt{while}\ x
باستخدام قاعدة while، يجب إثبات:
:\{x \leq 10 \wedge x ، أو مبسطة
:\{x ،
وهو ما يُستنتج بسهولة من قاعدة الإسناد.
وأخيراً، يمكن تبسيط الشرط اللاحق \{\neg x  إلى \{x=10\}.

كمثال آخر، يمكن استخدام قاعدة while للتحقق رسميًا من البرنامج الغريب التالي لحساب الجذر التربيعي الدقيق  لعدد عشوائي —حتى لو كانت  متغيرًا صحيحًا و عددًا غير مربعي:
:\{\texttt{true}\}   \texttt{while}\ x\cdot x \neq a\ \texttt{do}\ \texttt{skip}\ \texttt{done}   \{x \cdot x = a \wedge \texttt{true}\}
بعد تطبيق قاعدة while مع كون  هو ، يتبقى إثبات:
:\{\texttt{true} \wedge x\cdot x \neq a\}   \texttt{skip}   \{\texttt{true}\}،
وهو ما ينتج عن قاعدة التجاوز (skip) وقاعدة العاقبة.

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

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

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

:\dfrac{

في هذه القاعدة، بالإضافة إلى الحفاظ على ثبات الحلقة، يجب أيضًا إثبات إثبات التوقف عبر تعبير  يُعرف باسم متغيّر الحلقة، الذي تتناقص قيمته تناقصًا صارمًا وفق علاقة ترتيب  مؤسَّسة جيدًا على مجموعة  خلال كل تكرار.
وبما أن  مؤسسة جيدًا، فإن أي تسلسل تناقصي صارم لمتغيرات من  يكون نهائيًا؛ فلا يمكن أن يستمر  في التناقص إلى الأبد. (على سبيل المثال، الترتيب الاعتيادي  مؤسَّس جيدًا على الأعداد الصحيحة الموجبة \mathbb{N}، لكنه ليس كذلك على \mathbb{Z} ولا على \mathbb{R}^+؛ وكل هذه المجموعات تُفهم بالمعنى الرياضي لا الحاسوبي، وهي جميعًا لانهائية).

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

وبالرجوع إلى المثال الأول في القسم السابق، لإثبات الصحة الكلية لـ
:[x \leq 10]\texttt{while}\ x 
يمكن تطبيق قاعدة while للصحة الكلية باختيار  كالأعداد الصحيحة غير السالبة مع الترتيب الاعتيادي، والتعبير  كـ 10 - x، مما يتطلب بدوره إثبات:
:[x \leq 10 \wedge x 
وبتعبير غير رسمي، يجب إثبات أن المسافة 10-x تتناقص في كل دورة من الحلقة، بينما تظل غير سالبة؛ مما يعني أن هذه العملية لا يمكن أن تستمر إلا لعدد محدود من الدورات.

يمكن تبسيط هدف الإثبات السابق إلى:
:[x ،
ويمكن إثبات ذلك على النحو التالي:
:[x+1 \leq 10 \wedge 10-x-1  يتم الحصول عليها باستخدام قاعدة الإسناد،
ويمكن تقويتها إلى [x  باستخدام قاعدة النتيجة.

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

## انظر أيضًا

## ملاحظات

## المراجع

## البيبليوغرافيا
* 

* 

* 

* 

* 

* 

## روابط خارجية
* KeY-Hoare هو نظام تحقق شبه تلقائي مبني على المسستنتج KeY، ويتضمن حساب هور للغة بسيطة تعتمد على حلقة while.
* وحدة حساب هور في j-Algo (j-Algo على غيت هاب، j-Algo على سورس فورج) – تصور مرئي لحساب هور ضمن برنامج تصور الخوارزميات j-Algo.

تصنيف:علم الحاسوب في 1969
تصنيف:تحليل البرنامج الساكن