מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

3.1. הגדרות בסיסיות

עבור תוכנית P, מצב של תוכנית $plot:$\sigma $$ יוגדר כהשמה מסויימת למשתני התוכנית.

מרחב המצבים (state-space) הינו מספר המצבים האפשריים בתוכנית. מרחב המצבים הישיגים במערכת הינו מספר המצבים אליהם ניתן להגיע מהמצב ההתחלתי של המערכת.

ניסוח נוסף: מצב של תוכנית הינו פונקציה ממשתני התוכנית לתחום שבו הם מקבלים את ערכיהם.

משתני התוכנית: המשתנים יתוארו ע"י הווקטור: $plot:$\bar x = \left( {{x_1},{x_2},...,{x_n}} \right)$$ .
מצב התוכנית $plot:$\sigma $$ הינו פונקציה ממשתני התוכנית לתחום הערכים שלהם.

הערך של המשתנה במצב $plot:$\sigma $$ מסומן על ידי $plot:$\sigma \left( x \right)$$ . לדוגמא: $plot:$\sigma \left( x \right) = 5$$ .
מפרט הינו זוג טענות מהצורה $plot:$ < {q_1}\left( {\bar x} \right),{q_2}\left( {\bar x} \right) > $$ כאשר $plot:${q_1}\left( {\bar x} \right),{q_2}\left( {\bar x} \right)$$ הן טענות מתחשיב היחסים מעל משתני התוכנית $plot:$\bar x$$ . המשמעות של המפרט היא שתנאי הקדם $plot:${q_1}\left( {\bar x} \right)$$ גורר את קיום התנאי $plot:${q_2}\left( {\bar x} \right)$$ עם סיום התוכנית. ( $plot:${q_1}$$ המצב בתחילת התוכנית, $plot:${q_2}$$ המצב בסופה).

דוגמא: תהא תוכנית בעלת המשתנים $plot:$\left( {x,y,b} \right)$$ כאשר: $plot:$x \in \mathbb{N},x \in \mathbb{R},b \in \left\{ {T,F} \right\}$$ . מפרט לדוגמא יהיה $plot:\[\left\langle {x > 0 \wedge b = T,y > x \wedge b = F} \right\rangle \]$
דגש: צריך לשים לב שבמפרט המצב של $plot:$\bar x$$ ב- $plot:${q_1}$$ אינו המצב של $plot:$\bar x$$ ב- $plot:${q_2}$$ .