صحة خوارزمية
في علم الحاسوب النظري، يمكن التأكد من صحة خوارزمية ما، إذا كانت تلك الخوارزمية صحيحة بالنسبة لمواصفات معينة. يشير مصطلح الصحة الوظيفية Functional correctness إلى سلوك مدخلات ومخرجات الخوارزمية: أي من أجل كل المدخلات الممكنة نحصل على خرج صحيح.
وثمة فرق بين الصحة الكلية، التي تتطلب أيضاً انتهاء الخوارزمية، والصحة الجزئية، التي لا تتطلب سوى جواباً صحيحاً إذا كان ثمة جواب. وبرهان الانتهاء termination proof هو نوع من أنواع البرهان الرياضي الذي يلعب دوراً حاسماً في التحقق الشكلي لأن صحة الكلية لخوارزمية يعتمد على انتهائها.
على سبيل المثال، فإن من السهل كتابة برنامج صحيح جزئياً يبحث في الأعداد الصحيحة 1 ، 2 ، 3 ،... عن ظواهر معينة (مثل العدد الكامل 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 نظاماً شكلياً للتفكير الدقيق حول صحة برامج الحاسوب. لا يمكنه سوى إظهار الصحة الجزئية، ولا بد من توسعته ببرهان انتهاء منفصل.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
انظر أيضاً
