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

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

4.2. סמנטיקה

המטרה שלנו: הגדרת חישוב של תוכנית. לצורך כך נגדיר את מושג הקונפיגורציה ואת רלציית המעברים:

קונפיגורציה – זוג $plot:$C = \left\langle {l,\sigma } \right\rangle $$ כאשר plot:$l$ תווית המציינת את הצומת בתוכנית בו נמצא החישוב. $plot:$\sigma $$ הינו מצב (השמה למשתנים).

משמעות קונפיגורציה: הפקודה שנמצאת בצומת עם התווית plot:$l$ מתבצעת ממצב $plot:$\sigma $$ .

רלציית המעברים $plot:$ \to $$ בין קונפיגורציות

$plot:$\left\langle {l,\sigma } \right\rangle \to \left\langle {l',\sigma '} \right\rangle $$ אמ"מ קיימת קשת מ- plot:$l$ ל- plot:$l'$ בתוכנית ובנוסף מתקיים אחד מהתנאים הבאים:

ב- יש פונקצית אתחול וגם $plot:$\sigma ' = \sigma $$ .
ב- פקודת הצבה מהצורה $plot:$\bar x: = \bar e$$ ומתקיים $plot:$\sigma ' = \sigma \left[ {\bar x \leftarrow \sigma \left( {\bar e} \right)} \right]$$ .

$plot:$\sigma ' = \sigma \left[ {\bar x \leftarrow \sigma \left( {\bar e} \right)} \right]$$ הינה הצבה חלקית, בה מוחלפים ב- $plot:$\sigma $$ כל ערכי המשתנים המצוינים בווקטור.
ב- פונקצית בדיקה $plot:$B\left( {\bar x} \right)$$ , מתקיים $plot:$\sigma \left( B \right) = true$$ וגם קיימת קשת מ- ל- בתוכנית המסומנת , וכן $plot:$\sigma ' = \sigma $$ או $plot:$\sigma \left( B \right) = false$$ וגם קיימת קשת מ- ל- בתוכנית המסומנת , וכן $plot:$\sigma ' = \sigma $$ .

בנוסף: כאשר ב- plot:$l$ יש halt אין מעבר לאף קונפיגורציה אחרת.

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

הגדרת חישוב:

חישוב של תוכנית P מקונפיגורציה C מסומן $plot:$\pi \left( {P,C} \right)$$ הינו סידרה מקסימלית של קונפיגורציות $plot:${C_i}$$ כך ש- $plot:${C_0} = C$$ ולכל plot:$i$ מתקיים $plot:${C_i} \to {C_{i + 1}}$$ .

חישוב סופי תמיד יסתיים בקונפיגורציה עוצרת.

קונפיגורציה עוצרת: $plot:$C = \left\langle {l,\sigma } \right\rangle $$ היא קונפיגורציה עוצרת אם plot:$l$ מציינת צומת עצירה בתוכנית.

קונפיגורציה התחלתית: $plot:$C = \left\langle {l,\sigma } \right\rangle $$ היא קונפיגורציה התחלתית אם plot:$l$ מציינת את צומת האתחול בתוכנית.

עבור חישוב סופי $plot:$\psi $$ המסתיים בקונפיגורציה (עוצרת) $plot:$\left\langle {l,{\sigma _k}} \right\rangle $$ מגדירים את $plot:$Val\left( {{\sigma _k}} \right)$$ להיות $plot:${\sigma _k}$$ .