הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

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

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

6.4.2. תרגילים

תרגיל 1

אילו מהמבנים הבאים הם מודלים לנוסחה: plot:$\varphi  = A\left( {pU\left( {EqUm} \right)} \right)$?

1.

המבנה מספק את הנוסחה.

המצב היחיד מספק plot:$EqUm$ כי הוא מספק אתplot:$m$ ולכן הוא מספק את plot:$\varphi $



2.

המבנה לא מודל לנוסחה. plot:${S_1},{S_2} \vDash EqUm$ אבל plot:${S_0}\not  \vDash \varphi $ בגלל המסלול plot:${S_0} \to {S_0} \to {S_0} \to ...$.

3.

plot:${S_0},{S_4}| = P$, plot:${S_4},{S_2},{S_1}| = EqUm$. כל מסלול עבור דרך plot:${S_0},{S_1}$ ולכן כל מסלול מספק את plot:$\varphi $.

תרגיל 2

נתונות הנוסחאות: plot:${\varphi _1} = AXXp & {\varphi _2} = AXEXp$. האם plot:$?{\varphi _1} \Rightarrow {\varphi _2}$

תשובה: כן.

יהיו plot:$M,S$ כך ש-plot:$M,S \vDash {\varphi _1}$. לכל מסלול  רק ש-plot:${S_0} = S$ מתקיים plot:$\pi | = XXp$.

plot:$ \Leftarrow $ יהי plot:$\pi ' = {S'_0},{S'_1}...$ מסלול כלשהו ב-plot:$M$ שמתחיל ב-plot:$S$ כאמור plot:$\pi '| = XXp$

plot:$ \Leftarrow $ plot:${S'_1}| = EXp \Leftarrow \pi {'^1}| = Xp$

plot:$ \Leftarrow $ plot:${\pi '^1} = EXp$

plot:$ \Leftarrow $ plot:$\pi '| = XEXp$

הראינו זאת לכל plot:$\pi '$ שמתחיל ב-plot:$S$ ולכןplot:$M,S \vDash AXEXp = \varphi $



האם plot:${\varphi _2} \Rightarrow {\varphi _1}$?

תשובה: לא. דוגמה נגדית:

plot:$M,S| = {\varphi _2}$ אבל בגלל המסלול העליון.

תגיות המסמך:

לפרק הקודם6.4.1. הבעיה והאלגוריתם
לפרק הבא6.4.3. סיבוכיות בדיקת מודל
אין תגובות!
שיתוף:
| עוד