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

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

5.1.2. רלציית המעברים $plot:$ \to $$

רלציית המעברים $plot:$ \to $$ הינה הרלציה הקטנה ביותר המקיימת את ההגדרה האינדוקטיבית הבאה:

$plot:$\left\langle {x: = e,\sigma } \right\rangle \to \left\langle {E,\sigma \left[ {x \leftarrow \sigma \left( e \right)} \right]} \right\rangle $$
$plot:$\left\langle {skip,\sigma } \right\rangle \to \left\langle {E,\sigma } \right\rangle $$
לכל תוכנית T: אם $plot:$\left\langle {S,\sigma } \right\rangle \to \left\langle {S',\sigma '} \right\rangle $$ אז $plot:$\left\langle {S;T,\sigma } \right\rangle \to \left\langle {S';T,\sigma '} \right\rangle $$ .

החישוב של פקודה אינו תלוי בפקודות בהמשך.
חישוב של הינו חישוב של במלואו ולאחר מכן חישוב של .

$plot:$\begin{gathered} \left( {\sigma \vDash B} \right) \Rightarrow & \left\langle {{\text{if }}B{\text{ then }}{S_1}{\text{ else }}{S_2}{\text{ fi; }}\sigma } \right\rangle \to \left\langle {{S_1},\sigma } \right\rangle \hfill \\ else & \Rightarrow & \left\langle {{\text{if }}B{\text{ then }}{S_1}{\text{ else }}{S_2}{\text{ fi; }}\sigma } \right\rangle \to \left\langle {{S_2},\sigma } \right\rangle \hfill \\ \end{gathered} $$
אם $plot:$\sigma \not \vDash B$$ אזי $plot:$\left\langle {{\text{while }}B{\text{ do }}S{\text{ od, }}\sigma } \right\rangle \to \left\langle {E,\sigma } \right\rangle $$ .

אחרת: $plot:\[\left\langle {{\text{while }}B{\text{ do }}S{\text{ od, }}\sigma } \right\rangle \to \left\langle {S;{\text{while }}B{\text{ do }}S{\text{ od}},\sigma } \right\rangle \]$

הגדרה: $plot:$\xrightarrow{*}$$ הוא הסגור הטרנזיטיבי של $plot:$\xrightarrow{{}}$$ . אם נכתוב $plot:${C_1}\xrightarrow{*}{C_2}$$ המשמעות היא שניתן לעבור מ- $plot:${C_1}$$ ע"י מספר סופי של צעדים (כולל 0) ל- $plot:${C_2}$$ .

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

הערה: כל חישוב סופי מסתיים ב- $plot:$\left\langle {E,\sigma '} \right\rangle $$ - קונפיגורציה עוצרת.

הגדרה:

$plot:$Val\left( {\pi \left( C \right)} \right) = \left\{ {\begin{array}{*{20}{c}} {\sigma '} \hfill & {C\xrightarrow{*}\left\langle {E,\sigma '} \right\rangle } \hfill \\ \bot \hfill & {else} \hfill \\ \end{array} } \right.$$

הגדרה: המשמעות (סמנטיקה) של תוכנית S היא $plot:$M\left[ S \right]\left( \sigma \right) = Val\left( {\pi \left( {S,\sigma } \right)} \right)$$ .

דגש: נשים לב כי לפי ההגדרה, חישוב של B לוקח תמיד צעד אחד $plot:$ \Leftarrow $$ חישוב לא יכול "להתקע" ב-B

לפרק הקודם5.1.1. שפת תוכניות while

לפרק הבא5.1.3. למת החישובים

תגובות:

שם:	(התחברות)
נושא:
תוכן:
	אין לשלוח תגובות הכוללות מידע המפר את תנאי השימוש של אתר UnderWarrior לרבות דברי הסתה, דיבה וסגנון החורג מהטעם הטוב.
		אימות: