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'$ בתוכנית ובנוסף מתקיים אחד מהתנאים הבאים:

  1. ב-plot:$l$ יש פונקצית אתחול וגם plot:$\sigma ' = \sigma $.
  2. ב-plot:$l$ פקודת הצבה מהצורה 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 $ כל ערכי המשתנים המצוינים בווקטור.
  3. ב-plot:$l$ פונקצית בדיקה plot:$B\left( {\bar x} \right)$, מתקיים plot:$\sigma \left( B \right) = true$ וגם קיימת קשת מ-plot:$l$ ל-plot:$l'$ בתוכנית המסומנת plot:$T$, וכן plot:$\sigma ' = \sigma $ או plot:$\sigma \left( B \right) = false$ וגם קיימת קשת מ-plot:$l$ ל-plot:$l'$ בתוכנית המסומנת plot:$F$, וכן 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}$.

בהינתן חישוב בתוכנית יש מסלול יחיד שמתאים לו. בהינתן מסלול יכול להיות שאין חישוב שמתאים לו, או לחילופין יכולים להיות אין סוף חישובים מתאימים.

אין חישוב מתאים

אינסוף חישובים מתאימים





plot:${l_0} \to {l_1} \to {l_*}$







plot:${l_0} \to {l_1} \to {l_*}$

אין תגובות!
שיתוף:
| עוד