لغة الحفظ
لغة الأوامر المحمية ( GCL ) هي لغة برمجة وضعها إدسكار ديكسترا لدلالات محولات المسند في مقرر EWD472. [ 1 ] وهي تجمع مفاهيم البرمجة بطريقة موجزة. تسهل هذه اللغة تطوير البرنامج وبرهانه معًا، حيث تقود أفكار البرهان عملية التطوير؛ علاوة على ذلك، يمكن حساب أجزاء من البرنامج فعليًا .
من أهم خصائص لغة GCL خاصية عدم الحتمية . فعلى سبيل المثال، في عبارة if، قد تكون هناك عدة بدائل صحيحة، ويتم الاختيار أثناء وقت التشغيل، أي عند تنفيذ عبارة if. وهذا يُعفي المبرمج من اتخاذ خيارات غير ضرورية، ويُساعد في التطوير الرسمي للبرامج.
تتضمن لغة GCL عبارة الإسناد المتعدد. على سبيل المثال، يتم تنفيذ العبارة x, y:= y, xبتقييم قيم الجانب الأيمن أولاً، ثم تخزينها في متغيرات الجانب الأيسر. وبالتالي، تقوم هذه العبارة بتبديل قيم x و y .
تتناول الكتب التالية تطوير البرامج باستخدام لغة GCL :
- ديكسترا، إدجر دبليو. (1976). منهج البرمجة . برنتيس هول. ISBN 978-0132158718.
- غريس، د. (1981). علم البرمجة . سلسلة دراسات في علوم الحاسوب (باللغات الإنجليزية والإسبانية واليابانية والصينية والإيطالية والروسية). نيويورك: سبرينغر فيرلاغ. doi : 10.1007/978-1-4612-5983-1 . ISBN 978-0-387-96480-5. S2CID 37034126 .
- ديكسترا, إدسجر دبليو ; فيجن، ويم إتش جيه (1988). طريقة البرمجة . بوسطن، ماساتشوستس: Addison-Wesley Longman Publishing Co., Inc.، ص. 200. ردمك 978-0-201-17536-3.
- كالدوايج، آن (1990). البرمجة: اشتقاق الخوارزميات . برنتيس هول، إنك. ISBN 0132041081.
- كوهين، إدوارد (1990). ديفيد غريس (محرر). البرمجة في التسعينيات: مقدمة في حساب البرامج . نصوص ودراسات في علوم الحاسوب. سبرينغر فيرلاغ. doi : 10.1007/978-1-4613-9706-9 . ISBN 978-1-4613-9706-9. S2CID 1509875 .
قيادة محمية
يتألف الأمر المحمي من شرط منطقي أو شرط حماية ، وعبارة "محمية" به. لا تُنفذ العبارة إلا إذا كان شرط الحماية صحيحًا، لذا عند تحليل العبارة، يمكن افتراض صحة الشرط. وهذا يُسهّل إثبات أن البرنامج يفي بالمواصفات .
الأمر المحمي هو عبارة من الشكل G → S، حيث
- G عبارة عن اقتراح ، يُسمى الحارس
- S عبارة عن بيان
- إذا كانت قيمة G صحيحة، فإن S مؤهل للتنفيذ. في معظم بنى GCL، قد تحتوي أوامر محظورة متعددة على شروط صحيحة، ويتم اختيار واحد منها فقط بشكل عشوائي للتنفيذ.
- إذا كانت قيمة G خاطئة، فلن يتم تنفيذ S.
تخطي وإلغاء
تُعدّ عبارات skip و abort من العبارات المهمة في لغة الأوامر المحمية. تُعتبر abort عبارة غير مُعرّفة تعني: نفّذ أي شيء، ولا يشترط أن تُنهي البرنامج. تُستخدم هذه العبارة لوصف البرنامج عند صياغة البرهان، وفي هذه الحالة عادةً ما يفشل البرهان. أما skip فهي عبارة فارغة تعني: لا تفعل شيئًا. تُستخدم غالبًا عندما يتطلب بناء الجملة عبارةً ما، ولكن لا ينبغي أن تتغير حالة البرنامج .
بناء الجملة
يتخطى
إجهاض
علم الدلالة
- تخطي : لا تفعل شيئاً
- إجهاض : فعل أي شيء
يُسند قيمًا للمتغيرات .
بناء الجملة
v := E
أو
v 0 , v 1 , ..., v n := ه 0 , ه 1 , ..., ه n
أين
- v هي متغيرات البرنامج
- E هي تعبيرات من نفس نوع البيانات مثل المتغيرات المقابلة لها.
السلسال
يتم فصل العبارات بفاصلة منقوطة واحدة (؛)
الاختيار : إذا
الاختيار (الذي يُسمى غالبًا "الشرط" أو "عبارة if") هو قائمة من الأوامر المشروطة، يُختار منها أمر واحد للتنفيذ. إذا كان أكثر من شرط صحيحًا، تُختار عبارة واحدة عشوائيًا لتنفيذ شرطها الصحيح. إذا لم يكن أي شرط صحيحًا، تكون النتيجة غير مُحددة، أي تُعادل abort . ولأن شرطًا واحدًا على الأقل يجب أن يكون صحيحًا، فغالبًا ما تكون عبارة skip الفارغة ضرورية. لا تحتوي عبارة if fi على أي أوامر مشروطة، لذا لا يوجد شرط صحيح أبدًا. وبالتالي، فإن if fi تُعادل abort .
بناء الجملة
إذا G0 → S0 □ G1 → S1 ... □ Gn → Sn fi
علم الدلالة
عند تنفيذ عملية الاختيار، يتم تقييم الشروط. إذا لم يكن أي من الشروط صحيحًا ، يتم إيقاف عملية الاختيار، وإلا يتم اختيار أحد البنود التي تحتوي على شرط صحيح بشكل عشوائي ويتم تنفيذ عبارته.
تطبيق
لا تحدد لغة GCL آلية تنفيذ محددة. وبما أن الشروط لا يمكن أن يكون لها آثار جانبية ، واختيار الشرط تعسفي، فيمكن للتنفيذ تقييم الشروط بأي ترتيب واختيار الشرط الصحيح الأول ، على سبيل المثال.
أمثلة
بسيط
بلغة شبه رمزية :
إذا كانت قيمة a < b، فاجعل قيمة c تساوي True. وإلا، فعيّن قيمة c إلى خطأ.
بلغة الأوامر المحمية:
إذا كان أ < ب → ج := صحيح □ a ≥ b → c := false fi
استخدام التخطي
بلغة شبه رمزية:
إذا كانت قيمة الخطأ صحيحة، فقم بتعيين قيمة x إلى 0
بلغة الأوامر المحمية:
إذا حدث خطأ → x := 0 □خطأ ← تخطي fi
إذا تم حذف الحارس الثاني وكان الخطأ خطأ، فإن النتيجة هي الإجهاض.
المزيد من الحراس صحيح
إذا كان a ≥ b → max := a □ b ≥ a → max := b fi
إذا كانت قيمة a تساوي b، فسيتم اختيار إما a أو b كقيمة جديدة للقيمة القصوى، وستكون النتائج متساوية. مع ذلك، قد يجد البرنامج أن إحدى القيمتين أسهل أو أسرع من الأخرى. وبما أنه لا يوجد فرق بالنسبة للمبرمج، فإن أيًا من الطريقتين ستفي بالغرض.
التكرار : افعل
يتم عرض تنفيذ هذا التكرار، أو الحلقة، أدناه.
بناء الجملة
نفّذ G0 → S0 □ G1 → S1 ... □ Gn → Sn od
علم الدلالة
يتألف تنفيذ التكرار من تنفيذ صفر أو أكثر من التكرارات ، حيث يتكون التكرار من اختيار أمر محمي Gi → Si بشكل عشوائي ، بشرط Gi صحيح، ثم تنفيذ الأمر Si . وبالتالي، إذا كانت جميع الشروط خاطئة في البداية، ينتهي التكرار فورًا دون تنفيذ أي تكرار. أما تنفيذ التكرار do od ، الذي لا يحتوي على أوامر محمية، فيتمثل في تنفيذ صفر من التكرارات، لذا فإن do od يُكافئ skip .
أمثلة
خوارزمية إقليدس الأصلية
a, b := A, B; do a < b → b := b - a □ b < a → a := a - b od
ينتهي هذا التكرار عندما يكون a = b، وفي هذه الحالة يكون a و b هما القاسم المشترك الأكبر لـ A و B.
يرى ديكسترا في هذه الخوارزمية طريقة لمزامنة دورتين لا نهائيتين وبطريقة تجعل و تظل صحيحة.a := a - bb := b - aa≥0b≥0
a, b, x, y, u, v := A, B, 1, 0, 0, 1; do b ≠ 0 → q, r := a div b, a mod b; a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v od
ينتهي هذا التكرار عندما b = 0، وفي هذه الحالة تحمل المتغيرات حل هوية بيزو : xA + yB = gcd(A,B).
نوع غير حتمي
نفّذ a>b → a، b := b، a □ b>c → b, c := c, b □ c>d → c, d := d, c od
يستمر البرنامج في تبديل العناصر طالما أن أحدها أكبر من العنصر الذي يليه. هذا النوع من فرز الفقاعات غير الحتمي ليس أكثر كفاءة من نظيره الحتمي، ولكنه أسهل في الإثبات: فهو لا يتوقف قبل فرز العناصر، وفي كل خطوة يقوم بفرز عنصرين على الأقل.
x, y = 1, 1; نفّذ x ≠ n → إذا كان f(x) ≤ f(y) → x := x+1 □ f(x) ≥ f(y) → y := x; x := x+1 طعام
تجد هذه الخوارزمية القيمة 1 ≤ y ≤ n التي تكون عندها دالة عددية صحيحة معينة f ذات قيمة عظمى. ولا يتم تحديد الحساب أو الحالة النهائية بشكل فريد بالضرورة.
التطبيقات
البرامج صحيحة من خلال التصميم
أدى تعميم التوافق الرصدي للأوامر المحمية في شبكة إلى حساب التحسين . [ 2 ] وقد تم ميكنة ذلك في طرق رسمية مثل طريقة B التي تسمح باشتقاق البرامج رسميًا من مواصفاتها.
الدوائر غير المتزامنة
تُعدّ الأوامر المحمية مناسبة لتصميم الدوائر شبه غير الحساسة للتأخير، لأن التكرار يسمح بتأخيرات نسبية اختيارية لاختيار الأوامر المختلفة. في هذا التطبيق، تتكون بوابة منطقية تُشغّل العقدة y في الدائرة من أمرين محميين، كما يلي:
PullDownGuard → y := 0 PullUpGuard → y := 1
يمثل كل من PullDownGuard و PullUpGuard هنا دالتين لمدخلات البوابة المنطقية، حيث يصفان متى تقوم البوابة بسحب المخرج إلى الأسفل أو إلى الأعلى، على التوالي. وخلافًا لنماذج تقييم الدوائر التقليدية، فإن تكرار مجموعة من الأوامر المحمية (المقابلة لدائرة غير متزامنة) يمكن أن يصف بدقة جميع السلوكيات الديناميكية الممكنة لتلك الدائرة. وبناءً على النموذج المُختار لعناصر الدائرة الكهربائية، قد تكون هناك حاجة إلى قيود إضافية على الأوامر المحمية لضمان وصفها بشكل مُرضٍ تمامًا. وتشمل القيود الشائعة الاستقرار، وعدم التداخل، وعدم وجود أوامر ذاتية الإبطال. [ 3 ]
التحقق من النموذج
تُستخدم الأوامر المحمية ضمن لغة برمجة بروميلا ، والتي يستخدمها مدقق نموذج SPIN . يتحقق SPIN من صحة تشغيل تطبيقات البرامج المتزامنة.
آخر
تقوم وحدة Perl Commands::Guarded بتنفيذ نسخة حتمية ومصححة من أوامر Dijkstra المحمية.
مراجع
- ↑ ديجكسترا، إدسكار دبليو . "EWD472: الأوامر المحمية، وعدم الحتمية، والاشتقاق الرسمي للبرامج" (ملف PDF) . تم الاطلاع عليه بتاريخ 16 أغسطس 2006 .
- ↑ باك، رالف ج. (1978). "حول صحة خطوات التحسين في تطوير البرامج (أطروحة دكتوراه)" (ملف PDF) . مؤرشف من الأصل (ملف PDF) بتاريخ 20 يوليو 2011.
- ↑ مارتن، آلان ج. "توليف دوائر VLSI غير المتزامنة" .
- البرمجة المنطقية
- إدسكار دبليو. ديكسترا