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

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

5.1.3. למת החישובים

למת החישובים מתארת את הצורה של כל חישובי התוכנית האפשריים. יהי $plot:${C_0} = \left\langle {{S_0},{\sigma _0}} \right\rangle $$ :

אם $plot:${S_0}$$ הוא פעולה אטומית אז $plot:$\pi \left( {{C_0}} \right)$$ הוא מהצורה $plot:${C_0} \to {C_1}$$ כאשר $plot:${C_1}$$ היא קונפיגורציה סופית (עוצרת) שנקבעת על ידי $plot:$\left( 1 \right)$$ או $plot:$\left( 2 \right)$$ בהגדרת $plot:$ \to $$ .
$plot:${S_0} = {S_1};{S_2}$$ . ל- $plot:$\pi \left( {{C_0}} \right)$$ יש אחת משלוש צורות:

התבדרות $plot:${S_1}$$ : $plot:${C_0} \to {C_1} \to ...$$ כאשר $plot:${C_i} = \left\langle {{T_i};{S_2},{\sigma _i}} \right\rangle $$ ו- $plot:$i \geqslant 0,\left\langle {{T_i},{\sigma _i}} \right\rangle $$ הוא חישוב אינסופי ב- $plot:${S_1}$$ מ- $plot:${\sigma _0}$$ .
התבדרות $plot:${S_2}$$ : $plot:${C_0}\xrightarrow{*}\left\langle {{S_2},{\sigma _i}} \right\rangle \to {C_{i + 1}} \to ...$$ כאשר $plot:${C_j},j \geqslant i$$ הוא חישוב אינסופי של $plot:${S_2}$$ .
עצירה: $plot:${C_0}\xrightarrow{*}\left\langle {{S_2},{\sigma _i}} \right\rangle \xrightarrow{*}\left\langle {E,\sigma '} \right\rangle $$ כאשר $plot:${C_0}\xrightarrow{*}\left\langle {{S_2},{\sigma _i}} \right\rangle $$ מתאים לחישוב סופי של $plot:${S_1}$$ וגם $plot:$\left\langle {{S_2},{\sigma _i}} \right\rangle \xrightarrow{*}\left\langle {E,\sigma '} \right\rangle $$ הוא חישוב סופי של $plot:${S_2}$$ .

אם $plot:${S_0} = {\text{while }}B{\text{ do }}S{\text{ od}}$$ אז $plot:$\pi \left( {{C_0}} \right)$$ מהצורה:

עצירה מיידית: $plot:${C_0} \to \left\langle {E,{\sigma _0}} \right\rangle $$ אם $plot:${\sigma _0} \vDash \neg B$$ .
התבדרות בחוג (S): (S לא מסתיים) $plot:${C_0}\xrightarrow{*}\left\langle {{S_0},{\sigma _1}} \right\rangle \xrightarrow{*}...\xrightarrow{*}\left\langle {{S_0},{\sigma _k}} \right\rangle \to {C_{k + 1}} \to ...$$ כאשר $plot:${\sigma _j} \vDash B$$ לכל $plot:$0 \leqslant j \leqslant k$$ וכן $plot:$\left\langle {{S_0},{\sigma _j}} \right\rangle \to \left\langle {S;{S_0},{\sigma _j}} \right\rangle \xrightarrow{*}\left\langle {E;{S_0},{\sigma _{j + 1}}} \right\rangle $$ הוא חישוב סופי של מ- $plot:${\sigma _j}$$ ו- $plot:$\pi \left( {{C_{k + 1}}} \right)$$ הוא חישוב אינסופי של .
התבדרות החוג: (התנאי B תמיד מתקיים) $plot:${C_0}\xrightarrow{*}\left\langle {{S_0},{\sigma _1}} \right\rangle \xrightarrow{*}...\xrightarrow{*}\left\langle {{S_0},{\sigma _k}} \right\rangle \to ...$$ כאשר $plot:${\sigma _j} \vDash B$$ לכל $plot:$j \geqslant 0$$ וכן $plot:$\left\langle {{S_0},{\sigma _j}} \right\rangle \xrightarrow{*}\left\langle {E,{\sigma _{j + 1}}} \right\rangle $$ הינו חישוב סופי של מ- $plot:${\sigma _j}$$ .
עצירה: $plot:${C_0}\xrightarrow{*}\left\langle {{S_0},{\sigma _1}} \right\rangle \xrightarrow{*}...\xrightarrow{*}\left\langle {E,{\sigma _k}} \right\rangle $$ כאשר $plot:${\sigma _j} \vDash B,{\sigma _K} \vDash \neg B$$ לכל $plot:$0 \leqslant j < k$$ .

אם $plot:${S_0} = {\text{if }}B{\text{ then }}{S_1}{\text{ else }}{S_2}{\text{ fi}}$$ אז $plot:$\pi \left( {{C_0}} \right)$$ הינו מהצורה:

אם $plot:${\sigma _0} \vDash B$$ אז מבצעים חישוב של $plot:${S_1}$$ : $plot:$\left\langle {{S_0},{\sigma _0}} \right\rangle \xrightarrow{{}}\left\langle {{S_1},{\sigma _0}} \right\rangle \xrightarrow{*}...$$
אחרת מבצעים חישוב של $plot:${S_2}$$ : $plot:$\left\langle {{S_0},{\sigma _0}} \right\rangle \xrightarrow{{}}\left\langle {{S_2},{\sigma _0}} \right\rangle \xrightarrow{*}...$$