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

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

${\displaystyle \{P\}C\{Q\}}$

حيث ${\displaystyle P}$ و${\displaystyle Q}$ هما عبارتان شرطيّتان و${\displaystyle C}$ هو أمر برمجي.^{[note 1]} تُسمّى ${\displaystyle P}$ الشرط القبلي و${\displaystyle Q}$ الشرط البعدي: فعندما يتحقق الشرط القبلي، فإن تنفيذ الأمر ${\displaystyle C}$ يؤدي إلى تحقق الشرط البعدي. العبارات الشرطية هي صيغ في منطق الرتبة الأولى.

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

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

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

نقص آخر في المسلمات والقواعد المذكورة أعلاه هو أنها لا توفر أساسًا لإثبات أن البرنامج ينتهي بنجاح. فقد يكون سبب الفشل في الإنهاء وجود حلقة لا نهائية، أو خرق لحد معين يحدده التنفيذ، كمدى القيم العددية، أو حجم التخزين، أو حد زمني يفرضه نظام التشغيل. لذلك ينبغي تفسير التدوين “${\displaystyle P\{Q\}R}$” على أنه “بشرط أن ينتهي البرنامج بنجاح، فإن خصائص نتائجه موصوفة بواسطة ${\displaystyle R}$.” من السهل نسبيًا تعديل المسلمات بحيث لا يمكن استخدامها للتنبؤ بنتائج البرامج غير المنتهية؛ ولكن الاستخدام الفعلي للمسلمات سيعتمد حينها على معرفة العديد من خصائص التنفيذ، كحجم وسرعة الحاسوب، ومدى الأرقام، وتقنية التعامل مع تجاوز القيم. باستثناء إثبات تجنب الحلقات اللا نهائية، من الأفضل على الأرجح إثبات "الصحة الشرطية" للبرنامج والاعتماد على التنفيذ لإعطاء تحذير في حال اضطر إلى إيقاف تنفيذ البرنامج بسبب خرق حد من حدود التنفيذ.

— Hoare 1969، صفحات 578-579

تؤكد قاعدة العملية الفارغة أن التعليمة skip لا تُغيّر حالة البرنامج، لذا فإن أي شرط يتحقق قبل skip سيبقى محققًا بعدها.^{[note 2]}

${\displaystyle {\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}}$

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

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

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

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

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

• ${\displaystyle \{x+1=43\}y:=x+1\{y=43\}}$
• ${\displaystyle \{x+1\leq N\}x:=x+1\{x\leq N\}}$

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

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

${\displaystyle \{y=3\}x:=2\{y=3\}}$

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

تنطبق قاعدة التركيب على برنامجين ينفّذان بالتسلسل، S ثم T، ويُكتب ذلك ${\displaystyle S;T}$، حيث تُدعى Q بـ"الشرط الوسيط":^[4]

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

مثال:

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

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

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

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

${\displaystyle {\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\}}}}$

تنص القاعدة على أنه إذا تحققت ${\displaystyle Q}$ بعد كل من فرعي then وelse بشرط تحقيق ${\displaystyle P}$ و${\displaystyle B}$ أو نفي ${\displaystyle B}$، فإن ${\displaystyle Q}$ تتحقق بعد عبارة if...endif بأكملها.^[5] ويجب ألا يكون للشرط B أي آثار جانبية. مثال يُقدّم في القسم التالي.

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

لم تكن هذه القاعدة واردة في منشور هوار الأصلي.^[1] ومع ذلك، بما أن العبارة

${\displaystyle {\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}}$

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

${\displaystyle {\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}}}$

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

${\displaystyle {\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}\}}}}$

تُتيح هذه القاعدة تقوية الشرط المسبق ${\displaystyle P_{2}}$ و/أو إضعاف الشرط اللاحق ${\displaystyle Q_{2}}$. تُستخدم هذه القاعدة مثلاً لتحقيق تطابق حرفي بين الشرطين اللاحقين في جزئي then وelse.

على سبيل المثال، لإثبات ما يلي:

${\displaystyle \{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {endif}}\{0\leq x\leq 15\}}$

يجب تطبيق قاعدة الشرط، والتي بدورها تتطلب إثبات:

${\displaystyle \{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}}$، أو مبسطة

${\displaystyle \{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}}$

لجزء then، و

${\displaystyle \{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}}$، أو مبسطة

${\displaystyle \{x=15\}x:=0\{0\leq x\leq 15\}}$

لجزء else.

ومع ذلك، تتطلب قاعدة الإسناد في جزء then اختيار P كـ ${\displaystyle 0\leq x\leq 15}$؛ وبالتالي تطبيق القاعدة يُعطي:

${\displaystyle \{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}}$، وهو ما يعادل منطقياً

${\displaystyle \{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}}$.

وبالتالي، تُستخدم قاعدة العاقبة لتقوية الشرط المسبق ${\displaystyle \{-1\leq x<15\}}$ المستنتج من قاعدة الإسناد إلى ${\displaystyle \{0\leq x<15\}}$ المطلوب لقاعدة الشرط.

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

${\displaystyle \{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}}$، أو مكافئة

${\displaystyle \{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}}$،

لذلك يجب تطبيق قاعدة العاقبة بحيث يكون ${\displaystyle P_{1}}$ و${\displaystyle P_{2}}$ هما ${\displaystyle \{x=15\}}$ و${\displaystyle \{{\texttt {true}}\}}$ على التوالي، لتقوية الشرط المسبق مرة أخرى. وبتعبير غير رسمي، فإن تأثير قاعدة العاقبة هو "نسيان" أن ${\displaystyle \{x=15\}}$ كان معلوماً عند دخول جزء else، لأن قاعدة الإسناد المستخدمة لذلك الجزء لا تحتاج إلى هذه المعلومة.

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

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

على سبيل المثال، لإثبات:

${\displaystyle \{x\leq 10\}{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}\{\neg x<10\wedge x\leq 10\}}$

باستخدام قاعدة while، يجب إثبات:

${\displaystyle \{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}}$، أو مبسطة

${\displaystyle \{x<10\}x:=x+1\{x\leq 10\}}$،

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

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

${\displaystyle \{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}}$

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

${\displaystyle \{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}}$،

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

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

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

${\displaystyle {\dfrac {<\ {\text{ترتيب مؤسَّس جيدًا على المجموعة}}\ D\quad ,\quad [P\wedge B\wedge t\in D\wedge t=z]S[P\wedge t\in D\wedge t<z]}{[P\wedge t\in D]{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}[\neg B\wedge P\wedge t\in D]}}}$

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

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

^{[note 3]}

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

${\displaystyle [x\leq 10]{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}[\neg x<10\wedge x\leq 10]}$

يمكن تطبيق قاعدة while للصحة الكلية باختيار D كالأعداد الصحيحة غير السالبة مع الترتيب الاعتيادي، والتعبير t كـ ${\displaystyle 10-x}$، مما يتطلب بدوره إثبات:

${\displaystyle [x\leq 10\wedge x<10\wedge 10-x\geq 0\wedge 10-x=z]x:=x+1[x\leq 10\wedge 10-x\geq 0\wedge 10-x<z]}$

وبتعبير غير رسمي، يجب إثبات أن المسافة ${\displaystyle 10-x}$ تتناقص في كل دورة من الحلقة، بينما تظل غير سالبة؛ مما يعني أن هذه العملية لا يمكن أن تستمر إلا لعدد محدود من الدورات.

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

${\displaystyle [x<10\wedge 10-x=z]\quad x:=x+1\quad [x\leq 10\wedge 10-x<z]}$،

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

${\displaystyle [x+1\leq 10\wedge 10-x-1<z]\quad x:=x+1\quad [x\leq 10\wedge 10-x<z]}$ يتم الحصول عليها باستخدام قاعدة الإسناد،

ويمكن تقويتها إلى ${\displaystyle [x<10\wedge 10-x=z]}$ باستخدام قاعدة النتيجة.

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

<div style="-moz-column-count:

• التوكيد (تطوير البرمجيات)  ^{[لغات أخرى]}‏
• الدلالات التعيينية
• تصميم بالعقود
• المنطق الديناميكي  ^{[لغات أخرى]}‏
• التحقق الشكلي
• ثابت الحلقة  ^{[لغات أخرى]}‏
• دلالات محول القضايا  ^{[لغات أخرى]}‏
• تحليل البرنامج الساكن

-webkit-column-count

• التوكيد (تطوير البرمجيات)  ^{[لغات أخرى]}‏
• الدلالات التعيينية
• تصميم بالعقود
• المنطق الديناميكي  ^{[لغات أخرى]}‏
• التحقق الشكلي
• ثابت الحلقة  ^{[لغات أخرى]}‏
• دلالات محول القضايا  ^{[لغات أخرى]}‏
• تحليل البرنامج الساكن

column-count

• التوكيد (تطوير البرمجيات)  ^{[لغات أخرى]}‏
• الدلالات التعيينية
• تصميم بالعقود
• المنطق الديناميكي  ^{[لغات أخرى]}‏
• التحقق الشكلي
• ثابت الحلقة  ^{[لغات أخرى]}‏
• دلالات محول القضايا  ^{[لغات أخرى]}‏
• تحليل البرنامج الساكن;">{{{2}}}

• Apt، Krzysztof R.؛ Olderog، Ernst-Rüdiger (ديسمبر 2019). "Fifty years of Hoare's logic". Formal Aspects of Computing. ج. 31 ع. 6: 759. DOI:10.1007/s00165-019-00501-3. S2CID:102351597. مؤرشف من الأصل في 2024-09-15.

• Floyd، R. W. (1967). "Assigning meanings to programs" (PDF). Proceedings of the American Mathematical Society. Symposia on Applied Mathematics. ج. 19: 19–31. مؤرشف من الأصل (PDF) في 2025-03-19.

• Hoare، C. A. R. (أكتوبر 1969). "An Axiomatic Basis for Computer Programming". Communications of the ACM. ج. 12 ع. 10: 576–583. DOI:10.1145/363235.363259. S2CID:207726175.

• Huth، Michael؛ Ryan، Mark (26 أغسطس 2004). Logic in Computer Science: modelling and reasoning about systems (ط. second). مطبعة جامعة كامبريدج. ص. XIV, 427. ISBN:978-0521543101.

• Reynolds، John C. (2009) [1998]. Theories of Programming Languages. مطبعة جامعة كامبريدج. ISBN:9780521106979.

• Tennent، Robert D. (2002). Specifying Software. مطبعة جامعة كامبريدج. ص. XII, 289. ISBN:9780521004015. مؤرشف من الأصل في 2024-05-27. كتاب تعليمي يتضمن مقدمة لمنطق هوار

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