دلالات التشغيل

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

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

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

المناهج

قدم غوردون بلوتكين الدلالات الهيكلية التشغيلية، وقدم روبرت هيب وماتياس فيليزن سياقات الاختزال، وجيل كان الدلالات الطبيعية.

دلالات الخطوة الصغيرة

دلالات التشغيل الهيكلية

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

ومن الأمثلة البسيطة على ذلك، ندرس جزءًا من دلالات لغة برمجة بسيطة؛ قدمت التوضوحيات الموافقة في كتابي بلوتكين 81 وهينيسي 90، وغيرهما من الكتب. لنفترض أن C1 وC2 مجموعتان تصنفان برامج اللغة، وأن s تصنف الحالات (مثل الوظائف من مواقع الذاكرة إلى القيم). إذا كان لدينا تعبيرات (مصنفة حسب E) وقيم (V) ومواقع (L)، فستكون دلالات أمر تحديث الذاكرة على الشكل التالي:

${\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}$

تنص القاعدة على أنه «إذا اختزل التعبير E في الحالة s إلى القيمة V، فسيحدّث البرنامج L: = E الحالة مع تخصيص L = V».

يمكن كتابة دلالات التسلسل وفق القواعد الثلاثة التالية:

${\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}$

تنص القاعدة الأولى على أنه إذا انتهى البرنامج C1 في الحالة s إلى الحالة s'، فسيتم اختزال البرنامج C1;C2 في الحالة s إلى البرنامج C2 في الحالة s '. (يمكنك التفكير في هذا على أنه عملية تشكيل بحيث يمكنك تشغيل C1، ثم تشغيل C2 باستخدام مخزن الذاكرة الناتج.) تنص القاعدة الثانية على أنه إذا أمكن اختزال البرنامج C1 في الحالة s إلى البرنامج C1' في الحالة s'، سيختزل البرنامج C1; C2 في الحالة s إلى البرنامج C1;C2' في الحالة s'. (يمكنك التفكير في هذا على أنه تشكيل مبدأ لمترجم محسن: «يُسمح لك بتحويل C1 كما لو كانت قائمة بذاتها، حتى لو كان مجرد الجزء الأول من البرنامج.») تعتبر هذه الدلالات هيكلية، لأن معنى البرنامج التسلسلي C1; C2، يعرف بواسطة معنى C1 ومعنى C2.

إذا كان لدينا أيضًا تعبيرات منطقية للحالة، تصنف وفق B، فيمكننا تحديد دلالات الأمر while:

${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$

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

اكتسبت دلالات التشغيل الهيكلية، بفضل مظهرها البديهي وهيكلها سهل المتابعة، شعبية كبيرة وأصبحت معيارًا واقعيًا في تحديد دلالات التشغيل. ومن الألة على نجاحها هي اقتباس التقرير الأصلي (المسمى تقرير آرهوس) عن دلالات التشغيل الهيكلية (بلوتكين81) أكثر من 1000 مرة وفقًا لسايت سير (محرك بحث)، ما يجعله أحد أكثر التقارير الفنية استشهادًا في علوم الكمبيوتر.

دلالات الاختزال

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

$e=v\;|\;(e\;e)\;|\;x\quad \quad v=\lambda x.e\quad \quad C=\left[\,\right]\;|\;(C\;e)\;|\;(v\;C)$

تشتمل السياقات C على ثقب [ ] يمكن استخدامه لتوصيل الحد. يشير شكل السياقات إلى المكان الذي يمكن أن يحدث الاختزال (أي، يمكن توصيل حد بحد آخر). توفر البديهيات أو قواعد الاختزال، لوصف دلالات هذه اللغة:

$(\lambda x.e)\;v\longrightarrow e\,\left[x/v\right]\quad (\mathrm {\beta } )$

تعبر هذه البديهية المفردة عن قاعدة بيتا من تكامل لامدا. توضح سياقات الاختزال كيف تتكون هذه القاعدة بحدود أكثر تعقيدًا. يمكن استدعاء هذه القاعدة لموقع الوسيط لتطبيق مثل $((\lambda x.x\;\lambda x.x)\lambda x.(x\;x))$ بسبب وجود سياق  يطابق الحد. في هذه الحالة، تفكك السياقات الحدود بشكل فريد بحيث يمكن تطبيق اختزال واحد فقط في كل خطوة. إن توسيع البديهية لتتناسب مع سياقات الاختزال يعطي الإنهاء المتوافق. يعطي استيفاء الإنهاء الانعكاسي الانتقالي لهذه العلاقة علاقة الاختزال لهذه اللغة.

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