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

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

 

 

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