دلالات محول المسند

بالنسبة لعبارة S وشرط لاحق R ، فإن أضعف شرط مسبق هو مسند Q بحيث يكون لأي شرط مسبق P ،${\displaystyle \{P\}S\{R\}}$إذا وفقط إذا${\displaystyle P\Rightarrow Q}$بمعنى آخر، هو الشرط "الأقل تقييدًا" أو الأقل صرامة اللازم لضمان تحقق R بعد S. ويترتب على التفرد بسهولة من التعريف: إذا كان كل من Q و Q' من أضعف الشروط المسبقة، فإنه بحسب التعريف${\displaystyle \{Q'\}S\{R\}}$لذا${\displaystyle Q'\Rightarrow Q}$و${\displaystyle \{Q\}S\{R\}}$لذا${\displaystyle Q\Rightarrow Q'}$وبالتالي${\displaystyle Q=Q'}$نستخدم غالبًا${\displaystyle wp(S,R)}$للدلالة على أضعف شرط مسبق للعبارة S فيما يتعلق بشرط لاحق R.

نستخدم الرمز T للدلالة على المسند الصحيح في كل مكان، والرمز F للدلالة على المسند الخاطئ في كل مكان. يجب ألا نخلط بين هذا المفهوم والتعبير المنطقي المُعرَّف بقواعد لغة معينة، والذي قد يحتوي أيضًا على القيمتين true و false كقيم منطقية عددية. بالنسبة لهذه القيم العددية، نحتاج إلى تحويل نوعي بحيث يكون لدينا T = predicate(true) و F = predicate(false). غالبًا ما يتم هذا التحويل بشكل غير رسمي، لذا يميل الناس إلى اعتبار T صحيحًا و F خاطئًا.

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

• الإصدار 1:

${\displaystyle wp(x:=E,R)\ =\ (\forall yy=E\Rightarrow R[x\leftarrow y])}$ حيث يمثل y متغيرًا جديدًا وغير حر في E و R (يمثل القيمة النهائية للمتغير x )

• الإصدار 2:

بافتراض أن E محددة جيدًا، نطبق ما يسمى بقاعدة النقطة الواحدة على الإصدار 1. ثم

${\displaystyle wp(x:=E,R)\ =\ R[x\leftarrow E]}$

يتجنب الإصدار الأول احتمال تكرار x في R ، بينما يكون الإصدار الثاني أبسط عندما يكون هناك ظهور واحد على الأكثر لـ x في R. كما يكشف الإصدار الأول عن ازدواجية عميقة بين أضعف شرط مسبق وأقوى شرط لاحق (انظر أدناه).

مثال على حساب صحيح لـ wp (باستخدام الإصدار 2) لعمليات الإسناد مع متغير x ذي قيمة عددية صحيحة هو:

${\displaystyle {\begin{array}{rcl}wp(x:=x-5,x>10)&=&x-5>10\\&\Leftrightarrow &x>15\end{array}}}$

هذا يعني أنه لكي يتحقق الشرط اللاحق x > 10 بعد عملية الإسناد، يجب أن يتحقق الشرط المسبق x > 15 قبل عملية الإسناد. وهذا أيضًا هو "أضعف شرط مسبق"، لأنه "أضعف" قيد على قيمة x الذي يجعل x > 10 صحيحًا بعد عملية الإسناد.

${\displaystyle wp(S_{1};S_{2},R)\ =\ wp(S_{1},wp(S_{2},R))}$

على سبيل المثال،

${\displaystyle {\begin{array}{rcl}wp(x:=x-5;x:=x*2\ ,\ x>20)&=&wp(x:=x-5,wp(x:=x*2,x>20))\\&=&wp(x:=x-5,x*2>20)\\&=&(x-5)*2>20\\&=&x>15\end{array}}}$

${\displaystyle wp({\texttt {if}}\ E\ {\texttt {then}}\ S_{1}\ {\texttt {else}}\ S_{2}\ {\texttt {end}},R)\ =\ (E\Rightarrow wp(S_{1},R))\wedge (\neg E\Rightarrow wp(S_{2},R))}$

على سبيل المثال:

$// \wedge \ (\neg (x<y)\Rightarrow wp({\texttt {skip}},x\geq y))\\&=&(x<y\Rightarrow y\geq y)\ \wedge \ (\neg (x<y)\Rightarrow x\geq y)\\&\Leftrightarrow &{\texttt {true}}\end{array}}}$

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

• أن هناك تنفيذًا نهائيًا (على سبيل المثال، هناك تطبيق)،
• وأن الحالة النهائية لجميع عمليات التنفيذ المنتهية تفي بالشرط اللاحق.

إن تعريفات أضعف شرط مسبق المذكورة أعلاه (وخاصة بالنسبة لحلقة while ) تحافظ على هذه الخاصية.

اختيار

الاختيار هو تعميم لعبارة if :

${\displaystyle wp({\texttt {if}}\ E_{1}\rightarrow S_{1}\ [\!]\ \ldots \ [\!]\ E_{n}\rightarrow S_{n}\ {\texttt {fi}},R)\ ={\begin{array}{l}(E_{1}\vee \ldots \vee E_{n})\\\wedge \ (E_{1}\Rightarrow wp(S_{1},R))\\\ldots \\\wedge \ (E_{n}\Rightarrow wp(S_{n},R))\\\end{array}}}$

هنا، عندما كان هناك حارسان${\displaystyle E_{i}}$و${\displaystyle E_{j}}$إذا كانت هذه العبارات صحيحة في آن واحد، فيمكن تنفيذ أي من العبارات المرتبطة بها.${\displaystyle S_{i}}$أو${\displaystyle S_{j}}$.

يُوسّع حساب التحسين لغة GCL بمفهوم عبارة المواصفات . من الناحية التركيبية، نُفضّل كتابة عبارة المواصفات على النحو التالي:

${\displaystyle x:l[pre,post]}$

والتي تحدد عملية حسابية تبدأ في حالة تحقق الشرط pre وتضمن أن تنتهي في حالة تحقق الشرط post عن طريق تغيير x فقط . نسميها${\displaystyle l}$ثابت منطقي يُستخدم للمساعدة في تحديد المواصفات. على سبيل المثال، يمكننا تحديد عملية حسابية تزيد قيمة x بمقدار 1 كما يلي:

${\displaystyle x:l[x=l,x=l+1]}$

مثال آخر هو حساب الجذر التربيعي لعدد صحيح.

${\displaystyle x:l[x=l^{2},x=l]}$

تبدو عبارة التحديد بدائيةً بمعنى أنها لا تحتوي على عبارات أخرى. ومع ذلك، فهي معبرة للغاية، لأن الشرطين المسبق واللاحق عبارة عن مسندات اختيارية. وأضعف شرط مسبق لها هو كما يلي.

${\displaystyle wp(x:l[pre,post],R)=(\exists l::pre)\wedge (\forall s:(\forall l:pre:post(x\leftarrow s)):R(x\leftarrow s))}$ حيث s تعني طازج.

يجمع هذا الأسلوب بين فكرة مورغان النحوية وفكرة الحدة التي طرحها بيجلسما وماثيوز وويلتينك. ^{[ 1 ]} وتكمن ميزته الأساسية في قدرته على تعريف wp لأمر goto L وعبارات القفز الأخرى. ^{[ 2 ]}

يتطلب وضع صيغة رسمية لعبارات الانتقال مثل goto L عملية طويلة وشاقة. ويبدو أن الاعتقاد السائد يشير إلى أن عبارة goto لا يمكن تبريرها إلا من الناحية العملية. وربما يعود ذلك إلى عدم إدراك أن goto L في الواقع عبارة غير تقليدية (أي غير صارمة) ولا تتبع قانون ديكسترا "قانون استبعاد المعجزات" كما هو قائم بذاته. ولكنها تتمتع بنظرة عملية بسيطة للغاية من منظور أضعف الشروط المسبقة، وهو أمر غير متوقع. نُعرّف

${\displaystyle wp({\texttt {goto}}\ L,R)=wpL}$ حيث wpL هو أضعف شرط مسبق عند العلامة L.

بالنسبة لأمر goto L، ينقل التنفيذ التحكم إلى التسمية L التي يجب أن يتحقق عندها أضعف شرط مسبق. ولا ينبغي اعتبار طريقة الإشارة إلى wpL في القاعدة مفاجئة. إنها فقط${\displaystyle wp(L:S,Q)}$بالنسبة لقيمة Q المحسوبة حتى تلك النقطة. يشبه هذا أي قاعدة wp، حيث تستخدم عبارات مكونة لإعطاء تعريفات wp، على الرغم من أن goto L تبدو عملية بدائية. لا تتطلب القاعدة التفرد للمواقع التي يتحقق فيها wpL داخل البرنامج، لذا فهي تسمح نظريًا بظهور نفس التسمية في مواقع متعددة طالما أن أضعف شرط مسبق في كل موقع هو نفس wpL. يمكن لعبارة goto الانتقال إلى أي من هذه المواقع. هذا في الواقع يبرر أنه يمكننا وضع نفس التسميات في نفس الموقع عدة مرات، كما هو الحال في ...${\displaystyle S(L:L:S1)}$، وهو نفس الشيء${\displaystyle S(L:S1)}$كما أنه لا يتضمن أي قاعدة نطاق، مما يسمح بالقفز إلى داخل حلقة تكرارية، على سبيل المثال. لنحسب قيمة wp للبرنامج S التالي، الذي يتضمن قفزة إلى داخل حلقة تكرارية.

 wp(do x > 0 → L: x := x-1 od; if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi, post) = { قواعد التركيب والتناوب التسلسلي } wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; goto L, post)) ∨ (x ≥ 0 ∧ post) = { التركيب التسلسلي، الانتقال إلى، قواعد التعيين } wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post) = { قاعدة التكرار } الحل الأقوى لـ Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ] = { قاعدة التخصيص، تم إيجاد wpL = Z(x ← x-1) } الحل الأقوى لـ Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ post] = { استبدال } الحل الأقوى لـ Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ post ] = { حل المعادلة بالتقريب } post(x ← 0)

لذلك،

wp(S, post) = post(x ← 0).

يُعد الشرط الليبرالي الأضعف أحد المتغيرات المهمة لأضعف شرط مسبق${\displaystyle wlp(S,R)}$وهذا يُنتج أضعف شرطٍ إما أن لا تنتهي فيه S أو أن تُنشئ R. ولذلك، فهو يختلف عن wp في عدم ضمانه للإنهاء. ومن ثم، فهو يُطابق منطق هوار في صحته الجزئية: بالنسبة للغة العبارات المذكورة أعلاه، يختلف wlp عن wp فقط في حلقة while ، حيث لا يتطلب متغيرًا (انظر أعلاه).

بفرض أن S عبارة و R شرط مسبق (مسند على الحالة الأولية)، فإن ${\displaystyle sp(S,R)}$هو أقوى شرط لاحق لديهم : فهو يستلزم أي شرط لاحق تحققه الحالة النهائية لأي تنفيذ لـ S، لأي حالة ابتدائية تحقق R. بعبارة أخرى، ثلاثية هوار${\displaystyle \{P\}S\{Q\}}$يمكن إثبات ذلك في منطق هوار إذا وفقط إذا تحققت الشرطية التالية:

${\displaystyle \forall x,sp(S,P)\Rightarrow Q}$

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

${\displaystyle (\forall x,P\Rightarrow wlp(S,Q))\ \Leftrightarrow \ (\forall x,sp(S,P)\Rightarrow Q)}$

على سبيل المثال، لدينا في المهمة ما يلي:

${\displaystyle sp(x:=E,R)\ =\ \exists y,x=E[x\leftarrow y]\wedge R[x\leftarrow y]}$ حيث يكون y طازجًا

في المثال أعلاه، يمثل المتغير المنطقي y القيمة الأولية للمتغير x . وبالتالي،

${\displaystyle sp(x:=x-5,x>15)\ =\ \exists y,x=y-5\wedge y>15\ \Leftrightarrow \ x>10}$

في التسلسل، يبدو أن sp يعمل للأمام (بينما wp يعمل للخلف):

${\displaystyle sp(S_{1};S_{2}\ ,\ R)\ =\ sp(S_{2},sp(S_{1},R))}$

اقترح ليزلي لامبورت استخدام win و sin كمحولات للمسندات في البرمجة المتزامنة . ^{[ 3 ]}

تكون محولات المسند ذات الأهمية ( wp و wlp و sp ) رتيبة . يكون محول المسند S رتيبًا إذا وفقط إذا:

${\displaystyle (\forall x:P:Q)\Rightarrow (\forall x:S(P):S(Q))}$

ترتبط هذه الخاصية بقاعدة النتيجة في منطق هوار .

يكون محول المسند S صارمًا إذا وفقط إذا:

${\displaystyle S({\texttt {F}})\ \Leftrightarrow \ {\texttt {F}}}$

على سبيل المثال، يتم جعل wp صارمًا بشكل مصطنع، بينما لا يتم ذلك عادةً. على وجه الخصوص، إذا كان من غير الممكن إنهاء العبارة S،${\displaystyle wlp(S,{\texttt {F}})}$قابل للتنفيذ. لدينا

${\displaystyle wlp({\texttt {while}}\ {\texttt {true}}\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}},{\texttt {F}})\ \Leftrightarrow {\texttt {T}}}$

في الواقع، T هو ثابت صالح لتلك الحلقة.

تُسمى محولات المسند غير الصارمة، ولكنها رتيبة أو ترابطية، بالمعجزات، ويمكن استخدامها أيضًا لتعريف فئة من بنيات البرمجة، ولا سيما عبارات القفز، التي لم يُعرها ديكسترا اهتمامًا كبيرًا. تشمل عبارات القفز هذه الانتقال المباشر إلى L، وعبارات break وcontinue في حلقة تكرارية، وعبارات return في جسم إجراء، ومعالجة الاستثناءات، وما إلى ذلك. وقد تبيّن أن جميع عبارات القفز معجزات قابلة للتنفيذ، ^{[ 5 ]} أي أنه يمكن تنفيذها ولكنها ليست صارمة.

يكون محول المسند S منتهياً إذا:

${\displaystyle S({\texttt {T}})\ \Leftrightarrow \ {\texttt {T}}}$

في الواقع، لا يكون لهذا المصطلح معنى إلا بالنسبة لمحولات المسند الصارمة: في الحقيقة،${\displaystyle wp(S,{\texttt {T}})}$هو أضعف شرط مسبق يضمن إنهاء S.

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

يكون محول المسند S عطفيًا إذا وفقط إذا:

${\displaystyle S(P\wedge Q)\ \Leftrightarrow \ S(P)\wedge S(Q)}$

وينطبق هذا على${\displaystyle wp(S,.)}$، حتى لو كانت العبارة S غير حتمية كعبارة اختيار أو عبارة تحديد.

يكون محول المسند S منفصلاً إذا وفقط إذا:

${\displaystyle S(P\vee Q)\ \Leftrightarrow \ S(P)\vee S(Q)}$

هذا ليس هو الحال عموماً بالنسبة لـ${\displaystyle wp(S,.)}$عندما تكون العبارة S غير حتمية. في الواقع، لنفترض عبارة غير حتمية S تختار قيمة منطقية عشوائية. تُعطى هذه العبارة هنا على شكل عبارة الاختيار التالية :

${\displaystyle S\ =\ {\texttt {if}}\ {\texttt {true}}\rightarrow x:=0\ [\!]\ {\texttt {true}}\rightarrow x:=1\ {\texttt {fi}}}$

ثم،${\displaystyle wp(S,R)}$يُختزل إلى الصيغة${\displaystyle R[x\leftarrow 0]\wedge R[x\leftarrow 1]}$.

لذلك،${\displaystyle wp(S,\ x=0\vee x=1)}$يختزل إلى التكرار${\displaystyle (0=0\vee 0=1)\wedge (1=0\vee 1=1)}$

بينما الصيغة${\displaystyle wp(S,x=0)\vee wp(S,x=1)}$ يؤدي إلى الفرضية الخاطئة${\displaystyle (0=0\wedge 1=0)\vee (1=0\wedge 1=1)}$.

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

من بينها، تجمع نظرية أنواع هوار بين منطق هوار للغة شبيهة بلغة هاسكل ، ومنطق الفصل، ونظرية الأنواع . ^{[ 9 ]} يُنفذ هذا النظام كمكتبة روك تُسمى Ynot . ^{[ 10 ]} في هذه اللغة، يتوافق تقييم التعبيرات مع حسابات أقوى الشروط اللاحقة .

تُعدّ محوّلات المسند الاحتمالية امتدادًا لمحوّلات المسند للبرامج الاحتمالية . لهذه البرامج استخدامات عديدة في علم التشفير (إخفاء المعلومات باستخدام ضوضاء عشوائية)، والحوسبة الموزعة (كسر التناظر). ^{[ 11 ]}