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

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

4.4.1. הגדרות – טרנספורמצית המצבים, תנאי הישיגות

נתון מסלול: $plot:$\tau = {l_{i0}},{l_{i1}},...,{l_{in}}$$ . נרצה לחשב:

בהינתן מצב התוכנית ההתחלתי נרצה לדעת את מצב התוכנית הסופי.
בהינתן מצב התוכנית ההתחלתי נרצה לדעת האם המסלול עביר.

בהינתן מסלול $plot:$\tau = {l_{i0}},{l_{i1}},...,{l_{in}}$$ נגדיר:

טרנספורמציית המצבים (state transformer) $plot:${T_\tau }\left( {\bar x} \right)$$ על מסלול $plot:$\tau $$ שמתחיל ממצב $plot:$\bar x$$ . $plot:${T_\tau }\left( {\bar x} \right)$$ מתאר את המצב הסופי של התוכנית בעזרת המשתנים של תחילת התוכנית.
תנאי הישיגות (reachability condition) $plot:${R_\tau }\left( {\bar x} \right)$$ - ביטוי שערכו אם ורק אם $plot:$\tau $$ הוא מסלול עביר עבור המצב ההתחלתי $plot:$\bar x$$ .

משפט: בהינתן מסלול סופי $plot:$\tau = {l_{i0}},{l_{i1}},...,{l_{ik}}$$ שחישובו מתחיל ממצב $plot:${\sigma _0}$$ :

המסלול עביר (כלומר $plot:${l_{ik}}$$ ישיג מ- $plot:${l_{i0}}$$ לאורך המסלול $plot:$\tau $$ ) אם ורק אם $plot:${\sigma _0} \vDash {R_\tau }\left( {\bar x} \right)$$ .
אם המסלול מסתיים ב- $plot:${l_{ik}}$$ במצב $plot:${\sigma _k}$$ אזי מתקיים ש- $plot:${\sigma _k} = {\sigma _0}\left[ {\bar x \leftarrow {T_\tau }\left( {\bar x} \right)} \right]$$ .

שימוש: בהנתן מצב $plot:$\sigma $$ שנותן ערכים מסויימים למשתנים, ניתן לחשב את ערכם בסוף המסלול אם ביצענו אותו ממצב $plot:$\sigma $$ .

דוגמא: יהא $plot:${T_\tau }\left( {x,y} \right) = \left( {x + y,y} \right)$$ וגם $plot:${\sigma _0}\left( {x,y} \right) = \left( {2,4} \right)$$ אז $plot:${\sigma _k}\left( {x,y} \right) = \left( {6,4} \right)$$ .