صحة خوارزمية

في فهم الحاسوب النظري، يمكن التأكد من صحة خوارزمية ما، إذا كانت تلك الخوارزمية سليمة بالنسبة لمواصفات معينة. يشير مصطلح الصحة الوظيفية Functional correctness إلى سلوك مدخلات ومخرجات الخوارزمية: أي من أجل جميع المدخلات الممكنة نحصل على خرج سليم.

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

على سبيل المثال، فإن من السهل كتابة برنامج سليم جزئياً يبحث في الأعداد السليمة 1 ، 2 ، ثلاثة ،... عن ظواهر معينة (مثل العدد الكامل perfect number)، ولكن تأكيد الصحة الكلية يحتاج إثبات بعض الأمور التي لم يُتمكن بعض من التوصل إليها في نظرية الأعداد.

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

A deep result in proof theory, the Curry-Howard correspondence, states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus. Converting a proof in this way is called program extraction.

Hoare logic is a specific formal system for reasoning rigorously about the correctness of computer programs. It can only show partial correctness correctness and has to be augmented with a separate termination proof.

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