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

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

3.2. חישוב של תוכנית

חישוב של תוכנית P ממצב $plot:$\sigma $$ , המסומן על ידי $plot:$\pi \left( {P,\sigma } \right)$$ , הינו סדרה סופית של מצבים $plot:${\sigma _1},...,{\sigma _k}$$ או סדרה אינסופית של מצבים $plot:${\sigma _1},{\sigma _2},...$$ , המקיימים כי לכל plot:$i$ , המעבר מ- $plot:${\sigma _i}$$ אל $plot:${\sigma _{i + 1}}$$ הוא בהתאם לתוכנית P, וכן כי $plot:${\sigma _1} = \sigma $$ .

המצב הסופי של החישוב יסומן $plot:$Val\left( \pi \right)$$ . במידה והחישוב סופי, הרי ש- $plot:$Val\left( \pi \right) = {\sigma _k}$$ . במידה והחישוב הוא אינסופי נסמן $plot:$Val\left( \pi \right) = \bot $$ . הערך $plot:$ \bot $$ הוא ערך לא מוגדר, השונה מכל הערכים (Bottom).

הגדרה: עבור מצב $plot:$\sigma $$ וטענה $plot:$q\left( {\bar x} \right)$$ , נסמן $plot:$\sigma \vDash q\left( {\bar x} \right)$$ (המצב מספק את הנוסחה/טענה) אם הטענה $plot:$q\left( {\bar x} \right)$$ נכונה כאשר מציבים במקום המשתנים החופשיים ב- $plot:$q\left( {\bar x} \right)$$ את הערכים המתאימים להם ב- $plot:$\sigma $$ .

לדוגמא, תהי הטענה: $plot:$q\left( y \right) = \forall x\left( {x > y \vee x < y \vee x|2} \right)$$ מעל השלמים.

עבור המצב $plot:${\sigma _1}\left( y \right) = 1$$ מתקיים $plot:${\sigma _1}\not \vDash q\left( y \right)$$ . (במקרה בו ).
עבור $plot:${\sigma _2}\left( y \right) = 4$$ , מתקיים כי $plot:${\sigma _2} \vDash q\left( y \right)$$ .

נשים לב שאנחנו מדברים בדוגמא רק על המשתנה plot:$y$ מכיוון שרק משתנה זה הינו משתנה חופשי.

שיטת העבודה היא הצבת הערך של plot:$y$ בטענה, ובדיקה האם הטענה נכונה.

הגדרה: קבוצת מצבי התוכנית הינה הקבוצה הבאה: נסמן ב- $plot:${D_i}$$ את התחום של המשתנה ה- plot:$i$ בתוכנית. קבוצת המצבים הינה: $plot:${D_1} \times {D_2} \times ... \times {D_n} \cup \left\{ \bot \right\}$$ .

הגדרה: עבור כל טענה $plot:$q\left( {\bar x} \right)$$ , מתקיים כי $plot:$ \bot \not \vDash q\left( {\bar x} \right)$$ . (במקרה והתוכנית אינה עוצרת – אף טענה אינה מסתפקת). בפרט: