الصحة (علوم الحاسوب)

📅 آخر تحديث: ٢٤ يوليو ٢٠٢٦
✍️ نُشر في: ٢٤ يوليو ٢٠٢٦
الموسوعة الحرة

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

في إطار المفهوم الأخير، يُفرَّق بين الصحة الجزئية ، التي تشترط صحة الإجابة في حال إرجاعها، والصحة الكاملة ، التي تشترط أيضًا إرجاع إجابة في نهاية المطاف، أي انتهاء الخوارزمية. وبناءً على ذلك، لإثبات الصحة الكاملة لبرنامج ما، يكفي إثبات صحته الجزئية وانتهائه. [ 2 ] لا يمكن أتمتة هذا النوع الأخير من الإثبات ( إثبات الإنهاء ) بشكل كامل، لأن مشكلة التوقف غير قابلة للحل .

برنامج مكتوب بلغة C صحيح جزئيًا لإيجاد أصغر عدد فردي كامل، ولا يُعرف مدى صحته الكاملة حتى عام 2023.
// إرجاع مجموع القواسم الصحيحة للعدد n static int divisorSum ( int n ) { int i , sum = 0 ; for ( i = 1 ; i < n ; ++ i ) if ( n % i == 0 ) sum += i ; return sum ; } // إرجاع أصغر عدد فردي كامل int leastPerfectNumber ( void ) { int n ; for ( n = 1 ; ; n += 2 ) if ( n == divisorSum ( n )) return n ; }

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

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

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

منطق هوار هو نظام رسمي محدد للاستدلال بدقة حول صحة برامج الحاسوب. [ 3 ] وهو يستخدم تقنيات بديهية لتحديد دلالات لغة البرمجة والنقاش حول صحة البرامج من خلال تأكيدات تُعرف باسم ثلاثيات هوار.

اختبار البرمجيات هو أي نشاط يهدف إلى تقييم سمة أو قدرة لبرنامج أو نظام والتأكد من أنه يحقق النتائج المطلوبة. على الرغم من أهميته البالغة لجودة البرمجيات وانتشاره الواسع بين المبرمجين والمختبرين، إلا أن اختبار البرمجيات لا يزال فنًا نظرًا لمحدودية فهم مبادئ البرمجيات. تكمن صعوبة اختبار البرمجيات في تعقيدها، إذ لا يمكننا اختبار برنامج متوسط ​​التعقيد بشكل كامل. الاختبار ليس مجرد تصحيح الأخطاء، بل يمكن أن يكون هدفه ضمان الجودة، والتحقق من الصحة، وتقدير الموثوقية. كما يمكن استخدامه كمقياس عام. يُعد اختبار الصحة واختبار الموثوقية مجالين رئيسيين للاختبار. اختبار البرمجيات هو عملية موازنة بين الميزانية والوقت والجودة. [ 4 ]

انظر أيضاً

ملحوظات

  1. ↑ دانلوب، دوغلاس د.؛ باسيلي، فيكتور ر. (يونيو 1982). "تحليل مقارن للصحة الوظيفية" . اتصالات رابطة آلات الحوسبة . 14 (2): 229-244 . doi : 10.1145/356876.356881 . S2CID 18627112 . 
  2. ↑ مانا، زوهار؛ بنويلي، أمير (سبتمبر 1974). "النهج البديهي للصحة الكاملة للبرامج". مجلة أكتا إنفورماتيكا . 3 (3): 243-263 . doi : 10.1007/BF00288637 . S2CID 2988073 . 
  3. ↑ هوار، سي. أ. ر. (أكتوبر 1969). "أساس بديهي لبرمجة الحاسوب" . اتصالات رابطة آلات الحوسبة . 12 (10): 576-580 . doi : 10.1145/363235.363259 . S2CID 207726175 . 
  4. ↑ بان، جيانتاو (ربيع 1999). "اختبار البرمجيات" (مقرر دراسي). جامعة كارنيجي ميلون . تم الاطلاع عليه بتاريخ 21 نوفمبر 2017 .

مراجع