אימות תוכנה – הבדלי גרסאות

{{ניווט בהנדסת תוכנה}}

 

מרבית העוסקים ב[[פיתוח תוכנה]] [[בדיקות תוכנה|בודקים את התוכנה]] ולא מאמתים אותה. הבדיקה נעשית באמצעות בחירת מקרים ספציפיים ובדיקה שהתוכנה מתנהגת במקרים אלו כנדרש. שיטה זו כרוכה בעבודה רבה ורמת האמינות של תוכנה הנבדקת כך נמוכה יחסית. לעומת זאת, כאשר אנו מוכיחים את אמינות התוכנה אנו יודעים כי היא תתנהג נכון בכל המקרים, כולל כאלה שלא בדקנו.

 

ישנן שתי בעיות עיקריות באימות תוכנה. המעשית שבהן היא שאימות תוכנה דורש מיומנות רבה ורקע מתמטי ברמה גבוהה מהמקובל. הבעיה החמורה יותר היא שישנה הוכחה לכך שקיימות תוכניות שאי אפשר לאמת אותן. דוגמה לכך היא ההוכחה כי אי אפשר לפתח [[תוכנית מחשב|תוכנית]] שיכולה לוודא האם תוכנית כלשהי תעצור כאשר תקבל קלט מסוים (בעיה זו ידועה כ[[בעיית העצירה]]). לאור זאת בוודאי שאי אפשר להוכיח כי תוכנה לא תגיע למצב כלשהו.

למרות שמגבלה תיאורטית זו נראית חמורה עדיין אימות תוכנה תורם רבות מבחינה מעשית.

 

 

==ראו גם==

[[מונחים בתוכנה]]

 

[[קטגוריה:מדעי המחשב]]