دلالات التشغيل
المناهج > دلالات الخطوة الصغيرة > دلالات التشغيل الهيكلية

قدم غوردون بلوتكين دلالات التشغيل الهيكلية (إس أو إس، وتسمى أيضًا دلالات التشغيل المنظمة أو دلالات الخطوة الصغيرة) في (بلوتكين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 مرة وفقًا لسايت سير (محرك بحث)، ما يجعله أحد أكثر التقارير الفنية استشهادًا في علوم الكمبيوتر.