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

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

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