لماذا قاعدة الإسناد كما هي في Hoare Logic؟

Question

لماذا قاعدة التعيين كما هي في Hoare Logic/Axiomatic Semantics؟لا أستطيع أن أستوعب سبب تراجع قاعدة التعيين عما توقعته.

أفهم أن منطق Hoare يستخدم لإثبات المقترحات الرسمية لحالة البرنامج أثناء تنفيذ الأوامر.وهكذا، إذا قمنا بتنفيذ الأمر $$x:=e$$ كنت أتوقع أن التالي الدولة لديها مثل هذا الاستبدال...ولكن يبدو أن الاستبدال يحدث قبل نقوم بتنفيذ المهمة التي أجدها غريبة.كنت أتوقع:

$$ \{ P \} x:= e \{P[e/x]\}$$

بشرط $P$ هي تصريحات حول حالة البرنامج.

أنا متأكد من أن هناك تفسيرًا جيدًا لذلك وآسف إذا كان هذا سؤالًا أساسيًا، فأنا أعلم أنه يجب أن يكون كذلك.لكن هل يمكن لأحد أن يشرح لي ذلك؟

---

السؤال مكافأة:

لماذا لا نكتب قاعدة التعيين على النحو التالي:

$$ \{ Q \} x:= e \{Q[x/e]\}$$

لاحظ أنه ليس نفس اقتراحي الأصلي لأن لدينا $x$ و $e$ تبادلت حولها.أي.في حالة ما بعد أينما كان لدينا $e$ نضع $x$ (وهذا أمر جيد لأن البيان الذي ننفذه للتو هو ذلك $x$ يحمل قيمة $e$, ، لذلك ينبغي أن نكون قادرين على استبدال $e$ ل $x$ في حالة ما بعد إذا كان الشرط المسبق يساعد.

---

المشاركات ذات الصلة التي قرأتها والتي لم تساعد:

• هور الثلاثي للمهمة P{x/E} x:=E {P}
• منطق هور ويكيبيديا
• https://www.quora.com/unanswered/لماذا-is-the-signment-rule-the-way-it-is-in-Hoare-Logic
• https://www.reddit.com/r/ProgrammingLanguages/comments/e8suhh/why_is_the_signment_rule_the_way_it_is_in_hoare/

---

زائدة:

بالنسبة لنا نحن الذين يعانون من عسر القراءة، هذا هو ما يعنيه رمز الاستبدال في هذا السؤال:

$$ P[e/x] = P[e o x] $$

أي.استبدال كل حدوث مجاني ل $x$ مع التعبير/المصطلح/الشيء $e$.

Answer 1

لذلك بعد القراءة والتفكير في الأمر أكثر هذا هو شرحي (بفضل أسس البرمجيات):

يبدو أن الارتباك الرئيسي بالنسبة لي هو معنى $P[e/x]$ (يستبدل كل مثيل مجاني لـ x بـ e).ما يفعله هذا هو أينما ترى الرمز $x$ حرفيا إزالته ووضعه $e$.على سبيل المثال $ P[e/x] = (x+y+1)[e/x] o P[e/x] = (e+y+1)$ لذا لاحظ كيف $x$ اختفى حرفيا من $P$.إذن ما نريده هو بمجرد قيامنا بالمهمة:

$$ س:= ه$$

أن البيان صحيح إذا كان لدينا $x$ بدلاً من $e$.فإذا كانت القاعدة هي:

$$ \{ P[e/x] \} x:= e \{ P \}$$

ثم ما نريده هو، عندما نقوم بالتوصيل $x$ ل $e$ نريد أن يكون البيان في الاعتبار صحيحا.لذلك قبل أن نبدأ الكود الذي لدينا $P[e/x]$.ثم نقوم بتشغيل المهمة وجميع مثيلات $e$ تختفي ونحصل $x$ليحل محلهم.الذي - التي يجب يكون صحيحًا إذا كان الكود الذي تم تشغيله هو التعيين (منذ $x$ الآن احتفظ بالقيمة $e$, ، حتى تتمكن من إزالتها $e$والمكان $x$).

هذا هو تفسير المفهوم المجرد.دعونا (بلا خجل) نستخدم مثال الأسس البرمجية (SF):

{{ Y = 1 }} X ::= Y {{ X = 1 }} باللغة الإنجليزية:إذا بدأنا في حالة حيث قيمة Y هي 1 وقمنا بتعيين Y إلى X، فسننتهي في حالة حيث X هي 1.أي أن خاصية كونها تساوي 1 يتم نقلها من Y إلى X.

فقرة أخرى مفيدة من SF:

وبالمثل ، في {y + z = 1}} x :: = y + z {{x = 1}} يتم نقل نفس الخاصية (تساوي واحد) إلى x من التعبير y + z على اليد اليمنى جانب المهمة.بشكل عام ، إذا كان A هو أي تعبير حسابي ، فإن {{a = 1}} x :: = a {x = 1}} هو ثلاثية Hoare صالحة.

---

إضافة من الملاحظة الرائعة للتعليق:

من المهم أن ندرك أن القاعدة {p [e / x]} x: = e {p} تتيح كل من التعبير e والمتغير x في الحدوث postcondition.بمعنى آخر ، تتيح لك قاعدة الاستدلال استنتاج شرط ما بعد أن تم استبدال أي مجموعة فرعية من حوادث E في الشرط المسبق بـ X ، بما في ذلك أي منها.علاوة على ذلك، فهو يسمح لك باستنتاج كل هذه الشروط اللاحقة المختلفة في وقت واحد.

---

الرد على المكافأة لماذا

1) $ \{P[e/x]\} x:=e \{P\} $

افضل من

2) $ \{ Q \} x:=e \{Q[x/e]\} $:

إلى جانب النقطة الدقيقة المتمثلة في استبدال x بتعبيرات قد تكون غير مرئية (على سبيل المثال،e=0، هل يجب أن نستبدل $0$ مع عدد لا نهائي من $x$'س؟ماذا لو لم تكن الأصفار موجودة...يجب أن تكون القواعد نحوية ولكن أعتقد أنه من الأفضل تجنب مثل هذه الالتباسات)، أعتقد أن هذا هو السبب:

ما يجب أن تستوعبه قاعدة الإسناد هو أننا نقوم بإسناد التعبير e للمتغير x.وبالتالي، يجب "استبدال" x فقط بـ e.بشكل حدسي، في الكود (أو بشكل أكثر دقة حالة البرنامج $\سيجما$) عندما يبدأ x في الاحتفاظ بالقيمة e، فهذا لا يعني بشكل عشوائي أنه في كل مكان قد يوجد فيه e يصبح x بعد تنفيذ المهمة $x:=e$.في الحقيقة ما يعنيه ذلك هو أنه في حالة ما بعد لدينا علامة x.الآن يجب أن تكون قيمة علامات x هذه إذا لم تكن لدينا المهمة $e$ أي.نحن فقط "نتراجع" عن الاستبدال/التخصيص الذي قام به أمر التعيين.ليس كل تعبير عشوائي آخر ه.باختصار، الطريقة الوحيدة لمعرفة مكان وضع الحرف e الصحيح هي البدء بالحالة اللاحقة بعد الانتهاء من المهمة، ثم البدء من مكان e.إذا قمنا بذلك بشكل عكسي، فقد نستبدل e's التي لم نرغب في استبدالها (حتى لو كانت صحيحة على الأرجح، وهو ما أعتقد أنه ينبغي عليهم ذلك لأننا نقول أن x يحمل القيمة e بعد تعيين e إلى x).

Answer 2

لنفترض أننا نقوم بتشغيل البرنامج x := e, ، والسماح $\سيجما$ تكون الحالة الأولية، و $\سيجما'$ تكون الحالة النهائية.

الحدس الحاسم هنا هو:قيمة ال $x$ في ال أخير ولاية $\سيجما'$ هي نفس قيمة التعبير $e$ في ال أولي ولاية $\سيجما$.والواقع أن الأخير هو القيمة التي نسندها $x$ مع الأمر x := e.

وبالتالي، إذا $ف(-)$ هي خاصية على القيم، الصيغة $P(\mbox{$x$-in-the-final-state})$ يعادل $P(\mbox{$e$-in-the-initial-state})$.بعبارة أخرى $P(x)$ في ال postcondition (في الولاية $\سيجما'$) يعادل حقًا $P(ه)$ في ال شرط مسبق (في الولاية $\سيجما$).

يعد استخدام الاستبدال مجرد طريقة أكثر رسمية للنظر في الشرط اللاحق باعتباره "صيغة تعتمد على $x$"، أي.مثل $P(x)$, ، ثم يتطلب $P(ه)$ كشرط مسبق.