اشتقاق البرنامج

في علوم الحاسوب ، اشتقاق البرنامج هو اشتقاق البرنامج من مواصفاته، بالوسائل الرياضية.

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

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

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

يحاول اشتقاق البرنامج معالجة هذه العيوب من خلال:

تقصير البراهين، من خلال تطوير الرموز الرياضية المناسبة؛
اتخاذ قرارات التصميم من خلال المعالجة الرسمية للمواصفات.

المصطلحات التي تعتبر مرادفة تقريبًا لاشتقاق البرامج هي: البرمجة التحويلية، والخوارزميات، والبرمجة الاستنتاجية.

يُعدّ منهج بيرد -ميرتنز الرسمي نهجًا لاشتقاق البرامج.

تشمل أساليب تحقيق الدقة في الحوسبة الموزعة لغات بحثية مثل لغة البرمجة P.

انظر أيضاً

مراجع

Edsger W. Dijkstra ، Wim HJ Feijen، طريقة للبرمجة ، أديسون ويسلي، 1988، 188 صفحة
إدوارد كوهين، البرمجة في التسعينيات ، سبرينغر-فيرلاغ، 1990
آن كالدوايج، البرمجة: اشتقاق الخوارزميات ، برنتيس هول، 1990، 216 صفحة
ديفيد غريس، علم البرمجة ، سبرينغر-فيرلاغ، 1981، 350 صفحة
كارول مورغان (عالم حاسوب) ، البرمجة من المواصفات ، السلسلة الدولية في علوم الحاسوب (الطبعة الثانية)، برنتيس هول، 1998.
إريك سي آر هينر ، نظرية عملية للبرمجة ، 2008، 235 صفحة
إيه جيه إم فان جاستيرين. حول شكل الحجج الرياضية . سلسلة محاضرات في علوم الحاسوب رقم 445، سبرينغر-فيرلاغ، 1990. يعلم كيفية كتابة البراهين بوضوح ودقة.
مارتن ريم. "تمارين برمجة صغيرة"، ظهرت في علم برمجة الكمبيوتر ، المجلد 3 (1983) حتى المجلد 14 (1990).
رولاند باكهاوس. بناء البرامج: حساب التنفيذات من المواصفات . وايلي، 2003. ISBN 978-0-470-84882-1.
ديريك ج. كوري، بروس و. واتسون. منهج صحة البرمجة بالبناء . سبرينغر-فيرلاغ، 2012. ISBN 978-3-642-27919-5. يقدم شرحاً خطوة بخطوة لكيفية اشتقاق خوارزميات صحيحة رياضياً باستخدام تحسينات صغيرة وقابلة للمعالجة.