منطق هوار

تنص قاعدة العبارة الفارغة على أن عبارة التخطي لا تُغير حالة البرنامج، وبالتالي فإن أي شيء صحيح قبل التخطي يظل صحيحًا بعده. ^{[ ملاحظة 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]}$إذا كانت العبارة صحيحة قبل التخصيص، وفقًا لمسلمة التخصيص، فإن العبارة ستكون صحيحة بعد ذلك. والعكس صحيح.${\displaystyle P[E/x]}$خطأ (أي${\displaystyle \neg 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 y:=x+1}$لا يغير ذلك من حقيقة أن${\displaystyle x+1=43}$لذا، قد يظهر كلا البيانين في الشرط اللاحق. رسميًا، يتم الحصول على هذه النتيجة بتطبيق مخطط البديهيات مع كون P (${\displaystyle y=43}$و${\displaystyle x+1=43}$)، مما ينتج عنه${\displaystyle P[(x+1)/y]}$كون (${\displaystyle x+1=43}$و${\displaystyle x+1=43}$)، والتي يمكن بدورها تبسيطها إلى الشرط المسبق المحدد${\displaystyle x+1=43}$.

يُعادل مخطط بديهية التخصيص القول بأنه لإيجاد الشرط المسبق، يجب أولاً أخذ الشرط اللاحق واستبدال جميع حالات الطرف الأيسر من التخصيص بالطرف الأيمن منه. احذر من محاولة القيام بذلك بشكل عكسي باتباع هذه الطريقة الخاطئة في التفكير:${\displaystyle \{P\}x:=E\{P[E/x]\}}$تؤدي هذه القاعدة إلى أمثلة غير منطقية مثل:

${\displaystyle \{x=5\}x:=3\{3=5\}}$

قاعدة أخرى خاطئة تبدو مغرية للوهلة الأولى هي${\displaystyle \{P\}x:=E\{P\wedge x=E\}}$ويؤدي ذلك إلى أمثلة غير منطقية مثل:

${\displaystyle \{x=5\}x:=x+1\{x=5\wedge x=x+1\}}$

بينما يحدد شرط ما بعد معين P بشكل فريد الشرط المسبق${\displaystyle P[E/x]}$أما العكس فليس صحيحاً. على سبيل المثال:

• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}}$،
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}}$،
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}}$، و
• ${\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}}$

تُعدّ هذه أمثلة صحيحة لمخطط بديهية التخصيص.

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

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

يكون هذا خطأً إذا كان x و y يشيران إلى نفس المتغير ( التداخل )، على الرغم من أنه مثال صحيح لمخطط بديهية التخصيص (مع كليهما).${\displaystyle \{P\}}$و${\displaystyle \{P[2/x]\}}$كون${\displaystyle \{y=3\}}$).

التحقق من صحة رمز التبديل بدون متغيرات مساعدة

تُبدّل العبارات الثلاث التالية (الأسطر 2، 4، 6) قيم المتغيرين a و b ، دون الحاجة إلى متغير مساعد. في برهان التحقق، يُرمز إلى القيمة الابتدائية لـ a و b بالثابتين A و B على التوالي. يُفضّل قراءة البرهان عكسيًا، بدءًا من السطر 7؛ على سبيل المثال، يُستنتج السطر 5 من السطر 7 باستبدال a (التعبير المستهدف في السطر 6) بـ${\displaystyle ab}$(التعبير الأصلي في السطر 6). يتم استخدام بعض التبسيطات الحسابية ضمنيًا، وهي:${\displaystyle a-(ab)=b}$(السطر 5→3)، و${\displaystyle a+bb=a}$(السطر 3→1). رقم شفرة التأكيدات 1:    ${\displaystyle \{a=A\wedge b=B\}}$ 2: ${\displaystyle a:=a+b;}$    3: ${\displaystyle \{ab=A\wedge b=B\}}$ 4: ${\displaystyle b:=ab;}$ 5: ${\displaystyle \{b=A\wedge ab=B\}}$ 6: ${\displaystyle a:=ab}$ 7: ${\displaystyle \{b=A\wedge a=B\}}$

تنطبق قاعدة هوار للتركيب على البرامج التي يتم تنفيذها بالتسلسل S و T ، حيث يتم تنفيذ 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\}}}}$

تنص القاعدة الشرطية على أن الشرط اللاحق Q المشترك بين جزئي then و else هو أيضًا شرط لاحق لعبارة if...endif بأكملها . ^{[ 5 ]} في جزئي then و else ، يمكن إضافة الشرط B غير المنفي والمنفي إلى الشرط المسبق P ، على التوالي. يجب ألا يكون للشرط 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\}}$

بالنسبة للجزء السابق ، و

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

أما بالنسبة للجزء الآخر .

ومع ذلك، تتطلب قاعدة التخصيص للجزء "ثم" اختيار 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 ، لأن قاعدة التعيين المستخدمة لجزء 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\}}$

يتطلب تطبيق قاعدة "بينما" إثبات

${\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 صحيحًا ، يبقى إثبات

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

وهذا ما يترتب على قاعدة التخطي وقاعدة العواقب.

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

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

${\displaystyle {\dfrac {<\ {\text{is a well-founded ordering on the set}}\ 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 أكثر، أي أن فرضية القاعدة ستكون خاطئة. (هذه إحدى طرق التعبير عن الصحة الكاملة.) ^{[ ملاحظة 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]x:=x+1[x\leq 10\wedge 10-x<z]}$،

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

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

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

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