توحيد نظريات البرمجة

يتناول كتاب "توحيد نظريات البرمجة " ( UTP ) في علوم الحاسوب دلالات البرامج . ويوضح كيف يمكن دمج الدلالات التفسيرية والدلالات التشغيلية والدلالات الجبرية في إطار موحد للمواصفات الرسمية وتصميم وتنفيذ البرامج وأنظمة الحاسوب .

نُشر كتاب بهذا العنوان من تأليف كار هوار وهي جيفنغ ^{[ 1 ]} ضمن سلسلة برنتيس هول الدولية في علوم الحاسوب عام 1998، وهو متاح مجاناً على الإنترنت. ^{[ 2 ]}

بدأت سلسلة ندوات UTP في عام 2006. ^{[ 3 ]}

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

يُعرَّف برنامج الحاسوب بأنه أقوى صفة تصف كل ملاحظة ذات صلة يمكن إجراؤها على سلوك الحاسوب الذي يُنفِّذ ذلك البرنامج. ^{[ 4 ]}

في مصطلحات UTP، تُعرَّف النظرية بأنها نموذج لنمط برمجة معين. تتكون نظرية UTP من ثلاثة عناصر:

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

يُعد تحسين البرنامج مفهومًا مهمًا في برنامج UTP.${\displaystyle P_{1}}$يتم تحسينه بواسطة${\displaystyle P_{2}}$إذا وفقط إذا كانت كل ملاحظة يمكن إجراؤها من${\displaystyle P_{2}}$وهي أيضاً ملاحظة لـ${\displaystyle P_{1}}$يُعد تعريف التحسين شائعًا في جميع نظريات UTP:

${\displaystyle P_{1}\sqsubseteq P_{2}\quad {\text{إذا وفقط إذا}}\quad \left[P_{2}\Rightarrow P_{1}\right]}$

أين${\displaystyle \left[X\right]}$يشير ^{[ 5 ]} إلى الإغلاق الشامل لجميع المتغيرات في الأبجدية.

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

• المتغيرات غير المزخرفة (${\displaystyle v}$)، نمذجة عملية رصد البرنامج عند بدء تنفيذه؛ و
• المتغيرات المُهيأة (${\displaystyle v'}$)، نمذجة ملاحظة البرنامج في مرحلة لاحقة من تنفيذه.

يمكن تعريف بعض البنى اللغوية الشائعة في نظرية العلاقات على النحو التالي:

• يتم تصميم عبارة التخطي، التي لا تغير حالة البرنامج بأي شكل من الأشكال، على أنها هوية علائقية:

${\displaystyle \mathbf {skip} \equiv v'=v}$

• تحديد القيمة${\displaystyle E}$إلى متغير${\displaystyle a}$يتم تصميمها كإعداد${\displaystyle a'}$ل${\displaystyle E}$مع الاحتفاظ بجميع المتغيرات الأخرى (المشار إليها بـ${\displaystyle u}$) ثابت:

${\displaystyle a:=E\equiv a'=E\land u'=u}$

• إن التركيب التسلسلي لبرنامجين هو مجرد تركيب علائقي للحالة الوسيطة:

${\displaystyle P_{1};P_{2}\equiv \exists v_{0}\bullet P_{1}[v_{0}/v']\land P_{2}[v_{0}/v]}$

• إن الاختيار غير الحتمي بين البرامج هو الحد الأدنى الأقصى لها:

${\displaystyle P_{1}\sqcap P_{2}\equiv P_{1}\lor P_{2}}$

• يتم كتابة الاختيار المشروط بين البرامج باستخدام تدوين الوسط:

${\displaystyle P_{1}\triangleleft C\triangleright P_{2}\equiv (C\land P_{1})\lor (\lnot C\land P_{2})}$

• تُعطى دلالات الاستدعاء الذاتي بواسطة أصغر نقطة ثابتة${\displaystyle \mu \mathbf {F} }$محول مسند رتيب${\displaystyle \mathbf {F} }$:

${\displaystyle \mu X\bullet \mathbf {F} (X)\equiv \sqcap \left\{X\mid \mathbf {F} (X)\sqsubseteq X\right\}}$

• وودكوك، جيم ؛ كافالكانتي، آنا (2004). "مقدمة تعليمية للتصميمات في نظريات البرمجة الموحدة" (ملف PDF) . الأساليب الرسمية المتكاملة . سلسلة محاضرات في علوم الحاسوب ، المجلد  2999. سبرينغر. الصفحات 40-66 . doi : 10.1007/978-3-540-24756-2_4 . ISBN  978-3-540-21377-2.
• كافالكانتي، آنا؛ وودكوك، جيم (2006). "مقدمة تعليمية لـ CSP في نظريات البرمجة الموحدة" (ملف PDF) . تقنيات التحسين في هندسة البرمجيات . سلسلة محاضرات في علوم الحاسوب. المجلد  3167. سبرينغر. الصفحات 220-268 . doi : 10.1007/11889229_6 . ISBN  978-3-540-46253-8.

• موقع كتب UTP
• كتاب UTP على موقع Archive.org
• كتاب UTP في مكتبة الإنترنت المفتوحة