حساب التفاضل والتكامل الدقيق

حساب التحسين هو منهج رسمي للتحسين التدريجي لبناء البرامج. يتم تحديد السلوك المطلوب للبرنامج النهائي القابل للتنفيذ كبرنامج مجرد، وربما غير قابل للتنفيذ، والذي يتم تحسينه بعد ذلك من خلال سلسلة من التحويلات التي تحافظ على صحته ليصبح برنامجًا قابلاً للتنفيذ بكفاءة. ^{[ 1 ]}

ومن بين المؤيدين رالف يوهان باك ، الذي ابتكر هذا النهج في أطروحته للدكتوراه عام 1978 بعنوان "حول صحة خطوات التحسين في تطوير البرامج" ، وكارول مورغان ، وخاصةً من خلال كتابه "البرمجة من المواصفات" (برنتيس هول، الطبعة الثانية، 1994، ISBN 1). 0-13-123274-6في الحالة الأخيرة، كان الدافع هو ربط تدوين مواصفات أبريال Z ، عبر علاقة صارمة لتحسين البرنامج مع الحفاظ على السلوك ، بتدوين برمجة قابل للتنفيذ قائم على لغة أوامر ديكسترا المحمية . ويعني الحفاظ على السلوك في هذه الحالة أن أي ثلاثية هوار يحققها البرنامج يجب أن يحققها أيضًا أي تحسين له، وهو مفهوم يؤدي مباشرة إلى عبارات المواصفات كشروط مسبقة ولاحقة، قائمة بذاتها، لأي برنامج يمكن وضعه بينها بشكل سليم.